(0) Obligation:
JBC Problem based on JBC Program:
Manifest-Version: 1.0
Created-By: 1.6.0_20 (Apple Inc.)
Main-Class: Test10
public class Test10 {
public static void main(String[] args) {
rec(args.length);
}
private static void rec(long l) {
if (l > 0) {
for (int i = (int) l ; i < 100; i++)
test(i);
rec (l - 1);
}
}
private static void test(int i) {
descend(i);
descend(i);
descend(i);
descend(i);
descend(i);
descend(i);
descend(i);
descend(i);
}
private static void descend(int i) {
if (i > 0)
descend(i - 1);
}
}
(1) JBC2FIG (SOUND transformation)
Constructed FIGraph.
(2) Obligation:
FIGraph based on JBC Program:
Test10.main([Ljava/lang/String;)V: Graph of 13 nodes with 0 SCCs.
Test10.rec(J)V: Graph of 83 nodes with 1 SCC.
Test10.descend(I)V: Graph of 17 nodes with 0 SCCs.
(3) FIGtoITRSProof (SOUND transformation)
Transformed FIGraph SCCs to IDPs. Logs:
Log for SCC 0: Generated 9 rules for P and 7 rules for R.
Combined rules. Obtained 1 rules for P and 3 rules for R.
Filtered ground terms:
169_0_descend_LE(x1, x2, x3) → 169_0_descend_LE(x2, x3)
Cond_169_0_descend_LE(x1, x2, x3, x4) → Cond_169_0_descend_LE(x1, x3, x4)
220_0_descend_Return(x1) → 220_0_descend_Return
175_0_descend_Return(x1) → 175_0_descend_Return
Filtered duplicate args:
169_0_descend_LE(x1, x2) → 169_0_descend_LE(x2)
Cond_169_0_descend_LE(x1, x2, x3) → Cond_169_0_descend_LE(x1, x3)
Combined rules. Obtained 1 rules for P and 3 rules for R.
Finished conversion. Obtained 1 rules for P and 3 rules for R. System has predefined symbols.
Log for SCC 1: Generated 59 rules for P and 48 rules for R.
Combined rules. Obtained 10 rules for P and 22 rules for R.
Filtered ground terms:
69_0_rec_GE(x1, x2, x3, x4, x5) → 69_0_rec_GE(x2, x3, x4)
Cond_69_0_rec_GE1(x1, x2, x3, x4, x5, x6) → Cond_69_0_rec_GE1(x1, x3, x4, x5)
220_0_descend_Return(x1) → 220_0_descend_Return
321_0_descend_Load(x1, x2) → 321_0_descend_Load(x2)
309_0_descend_Load(x1, x2) → 309_0_descend_Load(x2)
295_0_descend_Load(x1, x2) → 295_0_descend_Load(x2)
282_0_descend_Load(x1, x2) → 282_0_descend_Load(x2)
266_0_descend_Load(x1, x2) → 266_0_descend_Load(x2)
250_0_descend_Load(x1, x2) → 250_0_descend_Load(x2)
237_0_descend_Load(x1, x2) → 237_0_descend_Load(x2)
92_0_descend_Load(x1, x2) → 92_0_descend_Load(x2)
Cond_69_0_rec_GE(x1, x2, x3, x4, x5, x6) → Cond_69_0_rec_GE(x1, x3, x4, x5)
175_0_descend_Return(x1) → 175_0_descend_Return
169_0_descend_LE(x1, x2, x3) → 169_0_descend_LE(x2, x3)
Cond_169_0_descend_LE(x1, x2, x3, x4) → Cond_169_0_descend_LE(x1, x3, x4)
143_0_rec_Return(x1) → 143_0_rec_Return
47_0_rec_Return(x1) → 47_0_rec_Return
327_0_descend_Return(x1) → 327_0_descend_Return
314_0_descend_Return(x1) → 314_0_descend_Return
300_0_descend_Return(x1) → 300_0_descend_Return
287_0_descend_Return(x1) → 287_0_descend_Return
273_0_descend_Return(x1) → 273_0_descend_Return
256_0_descend_Return(x1) → 256_0_descend_Return
243_0_descend_Return(x1) → 243_0_descend_Return
181_0_descend_Return(x1) → 181_0_descend_Return
Filtered duplicate args:
69_0_rec_GE(x1, x2, x3) → 69_0_rec_GE(x1, x3)
Cond_69_0_rec_GE1(x1, x2, x3, x4) → Cond_69_0_rec_GE1(x1, x2, x4)
Cond_321_2_rec_InvokeMethod(x1, x2, x3, x4, x5) → Cond_321_2_rec_InvokeMethod(x1, x2, x3, x5)
321_2_rec_InvokeMethod(x1, x2, x3, x4) → 321_2_rec_InvokeMethod(x1, x2, x4)
309_2_rec_InvokeMethod(x1, x2, x3, x4) → 309_2_rec_InvokeMethod(x1, x2, x4)
309_1_test_InvokeMethod(x1, x2, x3) → 309_1_test_InvokeMethod(x1, x3)
295_2_rec_InvokeMethod(x1, x2, x3, x4) → 295_2_rec_InvokeMethod(x1, x2, x4)
295_1_test_InvokeMethod(x1, x2, x3) → 295_1_test_InvokeMethod(x1, x3)
282_2_rec_InvokeMethod(x1, x2, x3, x4) → 282_2_rec_InvokeMethod(x1, x2, x4)
282_1_test_InvokeMethod(x1, x2, x3) → 282_1_test_InvokeMethod(x1, x3)
266_2_rec_InvokeMethod(x1, x2, x3, x4) → 266_2_rec_InvokeMethod(x1, x2, x4)
266_1_test_InvokeMethod(x1, x2, x3) → 266_1_test_InvokeMethod(x1, x3)
250_2_rec_InvokeMethod(x1, x2, x3, x4) → 250_2_rec_InvokeMethod(x1, x2, x4)
250_1_test_InvokeMethod(x1, x2, x3) → 250_1_test_InvokeMethod(x1, x3)
237_2_rec_InvokeMethod(x1, x2, x3, x4) → 237_2_rec_InvokeMethod(x1, x2, x4)
237_1_test_InvokeMethod(x1, x2, x3) → 237_1_test_InvokeMethod(x1, x3)
92_2_rec_InvokeMethod(x1, x2, x3, x4) → 92_2_rec_InvokeMethod(x1, x2, x4)
92_1_test_InvokeMethod(x1, x2, x3) → 92_1_test_InvokeMethod(x1, x3)
Cond_69_0_rec_GE(x1, x2, x3, x4) → Cond_69_0_rec_GE(x1, x2, x4)
169_0_descend_LE(x1, x2) → 169_0_descend_LE(x2)
Cond_169_0_descend_LE(x1, x2, x3) → Cond_169_0_descend_LE(x1, x3)
Filtered unneeded arguments:
Cond_69_0_rec_GE1(x1, x2, x3) → Cond_69_0_rec_GE1(x1, x2)
Combined rules. Obtained 10 rules for P and 22 rules for R.
Finished conversion. Obtained 10 rules for P and 22 rules for R. System has predefined symbols.
(4) Complex Obligation (AND)
(5) Obligation:
IDP problem:
The following function symbols are pre-defined:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
| ~ | Bwxor: (Integer, Integer) -> Integer |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
The following domains are used:
Integer
The ITRS R consists of the following rules:
169_0_descend_LE(
0) →
175_0_descend_Return191_1_descend_InvokeMethod(
175_0_descend_Return,
0) →
220_0_descend_Return191_1_descend_InvokeMethod(
220_0_descend_Return,
x0) →
220_0_descend_ReturnThe integer pair graph contains the following rules and edges:
(0):
169_0_DESCEND_LE(
x0[0]) →
COND_169_0_DESCEND_LE(
x0[0] > 0,
x0[0])
(1):
COND_169_0_DESCEND_LE(
TRUE,
x0[1]) →
169_0_DESCEND_LE(
x0[1] - 1)
(0) -> (1), if ((x0[0] > 0 →* TRUE)∧(x0[0] →* x0[1]))
(1) -> (0), if ((x0[1] - 1 →* x0[0]))
The set Q consists of the following terms:
169_0_descend_LE(
0)
191_1_descend_InvokeMethod(
175_0_descend_Return,
0)
191_1_descend_InvokeMethod(
220_0_descend_Return,
x0)
(6) IDPNonInfProof (SOUND transformation)
The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that
final constraints are written in
bold face.
For Pair
169_0_DESCEND_LE(
x0) →
COND_169_0_DESCEND_LE(
>(
x0,
0),
x0) the following chains were created:
- We consider the chain 169_0_DESCEND_LE(x0[0]) → COND_169_0_DESCEND_LE(>(x0[0], 0), x0[0]), COND_169_0_DESCEND_LE(TRUE, x0[1]) → 169_0_DESCEND_LE(-(x0[1], 1)) which results in the following constraint:
(1) (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ 169_0_DESCEND_LE(x0[0])≥NonInfC∧169_0_DESCEND_LE(x0[0])≥COND_169_0_DESCEND_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_169_0_DESCEND_LE(>(x0[0], 0), x0[0])), ≥))
We simplified constraint (1) using rule (IV) which results in the following new constraint:
(2) (>(x0[0], 0)=TRUE ⇒ 169_0_DESCEND_LE(x0[0])≥NonInfC∧169_0_DESCEND_LE(x0[0])≥COND_169_0_DESCEND_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_169_0_DESCEND_LE(>(x0[0], 0), x0[0])), ≥))
We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_169_0_DESCEND_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_12] + [(2)bni_12]x0[0] ≥ 0∧[(-1)bso_13] ≥ 0)
We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_169_0_DESCEND_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_12] + [(2)bni_12]x0[0] ≥ 0∧[(-1)bso_13] ≥ 0)
We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_169_0_DESCEND_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_12] + [(2)bni_12]x0[0] ≥ 0∧[(-1)bso_13] ≥ 0)
We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(6) (x0[0] ≥ 0 ⇒ (UIncreasing(COND_169_0_DESCEND_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_12 + (2)bni_12] + [(2)bni_12]x0[0] ≥ 0∧[(-1)bso_13] ≥ 0)
For Pair
COND_169_0_DESCEND_LE(
TRUE,
x0) →
169_0_DESCEND_LE(
-(
x0,
1)) the following chains were created:
- We consider the chain COND_169_0_DESCEND_LE(TRUE, x0[1]) → 169_0_DESCEND_LE(-(x0[1], 1)) which results in the following constraint:
(7) (COND_169_0_DESCEND_LE(TRUE, x0[1])≥NonInfC∧COND_169_0_DESCEND_LE(TRUE, x0[1])≥169_0_DESCEND_LE(-(x0[1], 1))∧(UIncreasing(169_0_DESCEND_LE(-(x0[1], 1))), ≥))
We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(8) ((UIncreasing(169_0_DESCEND_LE(-(x0[1], 1))), ≥)∧[2 + (-1)bso_15] ≥ 0)
We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(9) ((UIncreasing(169_0_DESCEND_LE(-(x0[1], 1))), ≥)∧[2 + (-1)bso_15] ≥ 0)
We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(10) ((UIncreasing(169_0_DESCEND_LE(-(x0[1], 1))), ≥)∧[2 + (-1)bso_15] ≥ 0)
We simplified constraint (10) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(11) ((UIncreasing(169_0_DESCEND_LE(-(x0[1], 1))), ≥)∧0 = 0∧[2 + (-1)bso_15] ≥ 0)
To summarize, we get the following constraints P
≥ for the following pairs.
- 169_0_DESCEND_LE(x0) → COND_169_0_DESCEND_LE(>(x0, 0), x0)
- (x0[0] ≥ 0 ⇒ (UIncreasing(COND_169_0_DESCEND_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_12 + (2)bni_12] + [(2)bni_12]x0[0] ≥ 0∧[(-1)bso_13] ≥ 0)
- COND_169_0_DESCEND_LE(TRUE, x0) → 169_0_DESCEND_LE(-(x0, 1))
- ((UIncreasing(169_0_DESCEND_LE(-(x0[1], 1))), ≥)∧0 = 0∧[2 + (-1)bso_15] ≥ 0)
The constraints for P
> respective P
bound are constructed from P
≥ where we just replace every occurence of "t ≥ s" in P
≥ by "t > s" respective "t ≥
c". Here
c stands for the fresh constant used for P
bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:
POL(TRUE) = 0
POL(FALSE) = 0
POL(169_0_descend_LE(x1)) = [-1]
POL(0) = 0
POL(175_0_descend_Return) = [-1]
POL(191_1_descend_InvokeMethod(x1, x2)) = [-1]
POL(220_0_descend_Return) = [-1]
POL(169_0_DESCEND_LE(x1)) = [2]x1
POL(COND_169_0_DESCEND_LE(x1, x2)) = [2]x2
POL(>(x1, x2)) = [-1]
POL(-(x1, x2)) = x1 + [-1]x2
POL(1) = [1]
The following pairs are in P
>:
COND_169_0_DESCEND_LE(TRUE, x0[1]) → 169_0_DESCEND_LE(-(x0[1], 1))
The following pairs are in P
bound:
169_0_DESCEND_LE(x0[0]) → COND_169_0_DESCEND_LE(>(x0[0], 0), x0[0])
The following pairs are in P
≥:
169_0_DESCEND_LE(x0[0]) → COND_169_0_DESCEND_LE(>(x0[0], 0), x0[0])
There are no usable rules.
(7) Complex Obligation (AND)
(8) Obligation:
IDP problem:
The following function symbols are pre-defined:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
| ~ | Bwxor: (Integer, Integer) -> Integer |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
The following domains are used:
Integer
The ITRS R consists of the following rules:
169_0_descend_LE(
0) →
175_0_descend_Return191_1_descend_InvokeMethod(
175_0_descend_Return,
0) →
220_0_descend_Return191_1_descend_InvokeMethod(
220_0_descend_Return,
x0) →
220_0_descend_ReturnThe integer pair graph contains the following rules and edges:
(0):
169_0_DESCEND_LE(
x0[0]) →
COND_169_0_DESCEND_LE(
x0[0] > 0,
x0[0])
The set Q consists of the following terms:
169_0_descend_LE(
0)
191_1_descend_InvokeMethod(
175_0_descend_Return,
0)
191_1_descend_InvokeMethod(
220_0_descend_Return,
x0)
(9) IDependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.
(10) TRUE
(11) Obligation:
IDP problem:
The following function symbols are pre-defined:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
| ~ | Bwxor: (Integer, Integer) -> Integer |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
The following domains are used:
Integer
The ITRS R consists of the following rules:
169_0_descend_LE(
0) →
175_0_descend_Return191_1_descend_InvokeMethod(
175_0_descend_Return,
0) →
220_0_descend_Return191_1_descend_InvokeMethod(
220_0_descend_Return,
x0) →
220_0_descend_ReturnThe integer pair graph contains the following rules and edges:
(1):
COND_169_0_DESCEND_LE(
TRUE,
x0[1]) →
169_0_DESCEND_LE(
x0[1] - 1)
The set Q consists of the following terms:
169_0_descend_LE(
0)
191_1_descend_InvokeMethod(
175_0_descend_Return,
0)
191_1_descend_InvokeMethod(
220_0_descend_Return,
x0)
(12) IDependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.
(13) TRUE
(14) Obligation:
IDP problem:
The following function symbols are pre-defined:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
| ~ | Bwxor: (Integer, Integer) -> Integer |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
The following domains are used:
Integer, Boolean
The ITRS R consists of the following rules:
92_0_descend_Load(
i12) →
181_0_descend_Return92_0_descend_Load(
i45) →
243_0_descend_Return92_0_descend_Load(
i59) →
256_0_descend_Return92_0_descend_Load(
i62) →
273_0_descend_Return92_0_descend_Load(
i67) →
287_0_descend_Return92_0_descend_Load(
i70) →
300_0_descend_Return92_0_descend_Load(
i74) →
314_0_descend_Return92_0_descend_Load(
i76) →
327_0_descend_Return92_0_descend_Load(
x0) →
169_0_descend_LE(
x0)
97_1_rec_InvokeMethod(
47_0_rec_Return,
0) →
143_0_rec_Return97_1_rec_InvokeMethod(
143_0_rec_Return,
x0) →
143_0_rec_Return169_0_descend_LE(
0) →
175_0_descend_Return169_0_descend_LE(
x0) →
Cond_169_0_descend_LE(
x0 > 0,
x0)
Cond_169_0_descend_LE(
TRUE,
x0) →
191_1_descend_InvokeMethod(
169_0_descend_LE(
x0 - 1),
x0 - 1)
191_1_descend_InvokeMethod(
175_0_descend_Return,
0) →
220_0_descend_Return191_1_descend_InvokeMethod(
220_0_descend_Return,
x0) →
220_0_descend_ReturnThe integer pair graph contains the following rules and edges:
(0):
69_0_REC_GE(
x0[0],
x1[0]) →
COND_69_0_REC_GE(
x1[0] < 100,
x0[0],
x1[0])
(1):
COND_69_0_REC_GE(
TRUE,
x0[1],
x1[1]) →
92_2_REC_INVOKEMETHOD(
92_1_test_InvokeMethod(
92_0_descend_Load(
x1[1]),
x1[1]),
x0[1],
x1[1])
(2):
92_2_REC_INVOKEMETHOD(
92_1_test_InvokeMethod(
220_0_descend_Return,
x0[2]),
x1[2],
x0[2]) →
237_2_REC_INVOKEMETHOD(
237_1_test_InvokeMethod(
92_0_descend_Load(
x0[2]),
x0[2]),
x1[2],
x0[2])
(3):
237_2_REC_INVOKEMETHOD(
237_1_test_InvokeMethod(
220_0_descend_Return,
x0[3]),
x1[3],
x0[3]) →
250_2_REC_INVOKEMETHOD(
250_1_test_InvokeMethod(
92_0_descend_Load(
x0[3]),
x0[3]),
x1[3],
x0[3])
(4):
250_2_REC_INVOKEMETHOD(
250_1_test_InvokeMethod(
220_0_descend_Return,
x0[4]),
x1[4],
x0[4]) →
266_2_REC_INVOKEMETHOD(
266_1_test_InvokeMethod(
92_0_descend_Load(
x0[4]),
x0[4]),
x1[4],
x0[4])
(5):
266_2_REC_INVOKEMETHOD(
266_1_test_InvokeMethod(
220_0_descend_Return,
x0[5]),
x1[5],
x0[5]) →
282_2_REC_INVOKEMETHOD(
282_1_test_InvokeMethod(
92_0_descend_Load(
x0[5]),
x0[5]),
x1[5],
x0[5])
(6):
282_2_REC_INVOKEMETHOD(
282_1_test_InvokeMethod(
220_0_descend_Return,
x0[6]),
x1[6],
x0[6]) →
295_2_REC_INVOKEMETHOD(
295_1_test_InvokeMethod(
92_0_descend_Load(
x0[6]),
x0[6]),
x1[6],
x0[6])
(7):
295_2_REC_INVOKEMETHOD(
295_1_test_InvokeMethod(
220_0_descend_Return,
x0[7]),
x1[7],
x0[7]) →
309_2_REC_INVOKEMETHOD(
309_1_test_InvokeMethod(
92_0_descend_Load(
x0[7]),
x0[7]),
x1[7],
x0[7])
(8):
309_2_REC_INVOKEMETHOD(
309_1_test_InvokeMethod(
220_0_descend_Return,
x0[8]),
x1[8],
x0[8]) →
321_2_REC_INVOKEMETHOD(
321_1_test_InvokeMethod(
92_0_descend_Load(
x0[8]),
x0[8]),
x1[8],
x0[8])
(9):
321_2_REC_INVOKEMETHOD(
321_1_test_InvokeMethod(
220_0_descend_Return,
x0[9]),
x1[9],
x0[9]) →
COND_321_2_REC_INVOKEMETHOD(
x0[9] > 0,
321_1_test_InvokeMethod(
220_0_descend_Return,
x0[9]),
x1[9],
x0[9])
(10):
COND_321_2_REC_INVOKEMETHOD(
TRUE,
321_1_test_InvokeMethod(
220_0_descend_Return,
x0[10]),
x1[10],
x0[10]) →
69_0_REC_GE(
x1[10],
x0[10] + 1)
(11):
69_0_REC_GE(
x0[11],
x1[11]) →
COND_69_0_REC_GE1(
x1[11] >= 100 && x0[11] > 0 && 1 > 0 && 0 < x0[11] - 1,
x0[11],
x1[11])
(12):
COND_69_0_REC_GE1(
TRUE,
x0[12],
x1[12]) →
69_0_REC_GE(
x0[12] - 1,
x0[12] - 1)
(0) -> (1), if ((x1[0] < 100 →* TRUE)∧(x0[0] →* x0[1])∧(x1[0] →* x1[1]))
(1) -> (2), if ((92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]) →* 92_1_test_InvokeMethod(220_0_descend_Return, x0[2]))∧(x0[1] →* x1[2])∧(x1[1] →* x0[2]))
(2) -> (3), if ((237_1_test_InvokeMethod(92_0_descend_Load(x0[2]), x0[2]) →* 237_1_test_InvokeMethod(220_0_descend_Return, x0[3]))∧(x1[2] →* x1[3])∧(x0[2] →* x0[3]))
(3) -> (4), if ((250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]) →* 250_1_test_InvokeMethod(220_0_descend_Return, x0[4]))∧(x1[3] →* x1[4])∧(x0[3] →* x0[4]))
(4) -> (5), if ((266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]) →* 266_1_test_InvokeMethod(220_0_descend_Return, x0[5]))∧(x1[4] →* x1[5])∧(x0[4] →* x0[5]))
(5) -> (6), if ((282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]) →* 282_1_test_InvokeMethod(220_0_descend_Return, x0[6]))∧(x1[5] →* x1[6])∧(x0[5] →* x0[6]))
(6) -> (7), if ((295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]) →* 295_1_test_InvokeMethod(220_0_descend_Return, x0[7]))∧(x1[6] →* x1[7])∧(x0[6] →* x0[7]))
(7) -> (8), if ((309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]) →* 309_1_test_InvokeMethod(220_0_descend_Return, x0[8]))∧(x1[7] →* x1[8])∧(x0[7] →* x0[8]))
(8) -> (9), if ((321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]) →* 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]))∧(x1[8] →* x1[9])∧(x0[8] →* x0[9]))
(9) -> (10), if ((x0[9] > 0 →* TRUE)∧(321_1_test_InvokeMethod(220_0_descend_Return, x0[9]) →* 321_1_test_InvokeMethod(220_0_descend_Return, x0[10]))∧(x1[9] →* x1[10])∧(x0[9] →* x0[10]))
(10) -> (0), if ((x1[10] →* x0[0])∧(x0[10] + 1 →* x1[0]))
(10) -> (11), if ((x1[10] →* x0[11])∧(x0[10] + 1 →* x1[11]))
(11) -> (12), if ((x1[11] >= 100 && x0[11] > 0 && 1 > 0 && 0 < x0[11] - 1 →* TRUE)∧(x0[11] →* x0[12])∧(x1[11] →* x1[12]))
(12) -> (0), if ((x0[12] - 1 →* x0[0])∧(x0[12] - 1 →* x1[0]))
(12) -> (11), if ((x0[12] - 1 →* x0[11])∧(x0[12] - 1 →* x1[11]))
The set Q consists of the following terms:
92_0_descend_Load(
x0)
97_1_rec_InvokeMethod(
47_0_rec_Return,
0)
97_1_rec_InvokeMethod(
143_0_rec_Return,
x0)
169_0_descend_LE(
x0)
Cond_169_0_descend_LE(
TRUE,
x0)
191_1_descend_InvokeMethod(
175_0_descend_Return,
0)
191_1_descend_InvokeMethod(
220_0_descend_Return,
x0)
(15) IDPNonInfProof (SOUND transformation)
The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that
final constraints are written in
bold face.
For Pair
69_0_REC_GE(
x0,
x1) →
COND_69_0_REC_GE(
<(
x1,
100),
x0,
x1) the following chains were created:
- We consider the chain 69_0_REC_GE(x0[0], x1[0]) → COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0]), COND_69_0_REC_GE(TRUE, x0[1], x1[1]) → 92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]), x0[1], x1[1]) which results in the following constraint:
(1) (<(x1[0], 100)=TRUE∧x0[0]=x0[1]∧x1[0]=x1[1] ⇒ 69_0_REC_GE(x0[0], x1[0])≥NonInfC∧69_0_REC_GE(x0[0], x1[0])≥COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])∧(UIncreasing(COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥))
We simplified constraint (1) using rule (IV) which results in the following new constraint:
(2) (<(x1[0], 100)=TRUE ⇒ 69_0_REC_GE(x0[0], x1[0])≥NonInfC∧69_0_REC_GE(x0[0], x1[0])≥COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])∧(UIncreasing(COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥))
We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3) ([99] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_75 + (-1)Bound*bni_75] + [(2)bni_75]x0[0] ≥ 0∧[(-1)bso_76] ≥ 0)
We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4) ([99] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_75 + (-1)Bound*bni_75] + [(2)bni_75]x0[0] ≥ 0∧[(-1)bso_76] ≥ 0)
We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5) ([99] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_75 + (-1)Bound*bni_75] + [(2)bni_75]x0[0] ≥ 0∧[(-1)bso_76] ≥ 0)
We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(6) ([99] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(2)bni_75] = 0∧[(-1)bni_75 + (-1)Bound*bni_75] ≥ 0∧0 = 0∧[(-1)bso_76] ≥ 0)
We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
(7) ([99] + x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(2)bni_75] = 0∧[(-1)bni_75 + (-1)Bound*bni_75] ≥ 0∧0 = 0∧[(-1)bso_76] ≥ 0)
(8) ([99] + [-1]x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(2)bni_75] = 0∧[(-1)bni_75 + (-1)Bound*bni_75] ≥ 0∧0 = 0∧[(-1)bso_76] ≥ 0)
For Pair
COND_69_0_REC_GE(
TRUE,
x0,
x1) →
92_2_REC_INVOKEMETHOD(
92_1_test_InvokeMethod(
92_0_descend_Load(
x1),
x1),
x0,
x1) the following chains were created:
- We consider the chain COND_69_0_REC_GE(TRUE, x0[1], x1[1]) → 92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]), x0[1], x1[1]) which results in the following constraint:
(9) (COND_69_0_REC_GE(TRUE, x0[1], x1[1])≥NonInfC∧COND_69_0_REC_GE(TRUE, x0[1], x1[1])≥92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]), x0[1], x1[1])∧(UIncreasing(92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]), x0[1], x1[1])), ≥))
We simplified constraint (9) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(10) ((UIncreasing(92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]), x0[1], x1[1])), ≥)∧[(-1)bso_78] ≥ 0)
We simplified constraint (10) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(11) ((UIncreasing(92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]), x0[1], x1[1])), ≥)∧[(-1)bso_78] ≥ 0)
We simplified constraint (11) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(12) ((UIncreasing(92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]), x0[1], x1[1])), ≥)∧[(-1)bso_78] ≥ 0)
We simplified constraint (12) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(13) ((UIncreasing(92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]), x0[1], x1[1])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_78] ≥ 0)
For Pair
92_2_REC_INVOKEMETHOD(
92_1_test_InvokeMethod(
220_0_descend_Return,
x0),
x1,
x0) →
237_2_REC_INVOKEMETHOD(
237_1_test_InvokeMethod(
92_0_descend_Load(
x0),
x0),
x1,
x0) the following chains were created:
- We consider the chain 92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(220_0_descend_Return, x0[2]), x1[2], x0[2]) → 237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(92_0_descend_Load(x0[2]), x0[2]), x1[2], x0[2]) which results in the following constraint:
(14) (92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(220_0_descend_Return, x0[2]), x1[2], x0[2])≥NonInfC∧92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(220_0_descend_Return, x0[2]), x1[2], x0[2])≥237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(92_0_descend_Load(x0[2]), x0[2]), x1[2], x0[2])∧(UIncreasing(237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(92_0_descend_Load(x0[2]), x0[2]), x1[2], x0[2])), ≥))
We simplified constraint (14) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(15) ((UIncreasing(237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(92_0_descend_Load(x0[2]), x0[2]), x1[2], x0[2])), ≥)∧[(-1)bso_80] ≥ 0)
We simplified constraint (15) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(16) ((UIncreasing(237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(92_0_descend_Load(x0[2]), x0[2]), x1[2], x0[2])), ≥)∧[(-1)bso_80] ≥ 0)
We simplified constraint (16) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(17) ((UIncreasing(237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(92_0_descend_Load(x0[2]), x0[2]), x1[2], x0[2])), ≥)∧[(-1)bso_80] ≥ 0)
We simplified constraint (17) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(18) ((UIncreasing(237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(92_0_descend_Load(x0[2]), x0[2]), x1[2], x0[2])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_80] ≥ 0)
For Pair
237_2_REC_INVOKEMETHOD(
237_1_test_InvokeMethod(
220_0_descend_Return,
x0),
x1,
x0) →
250_2_REC_INVOKEMETHOD(
250_1_test_InvokeMethod(
92_0_descend_Load(
x0),
x0),
x1,
x0) the following chains were created:
- We consider the chain 237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(220_0_descend_Return, x0[3]), x1[3], x0[3]) → 250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]), x1[3], x0[3]) which results in the following constraint:
(19) (237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(220_0_descend_Return, x0[3]), x1[3], x0[3])≥NonInfC∧237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(220_0_descend_Return, x0[3]), x1[3], x0[3])≥250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]), x1[3], x0[3])∧(UIncreasing(250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]), x1[3], x0[3])), ≥))
We simplified constraint (19) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(20) ((UIncreasing(250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]), x1[3], x0[3])), ≥)∧[(-1)bso_82] ≥ 0)
We simplified constraint (20) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(21) ((UIncreasing(250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]), x1[3], x0[3])), ≥)∧[(-1)bso_82] ≥ 0)
We simplified constraint (21) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(22) ((UIncreasing(250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]), x1[3], x0[3])), ≥)∧[(-1)bso_82] ≥ 0)
We simplified constraint (22) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(23) ((UIncreasing(250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]), x1[3], x0[3])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_82] ≥ 0)
For Pair
250_2_REC_INVOKEMETHOD(
250_1_test_InvokeMethod(
220_0_descend_Return,
x0),
x1,
x0) →
266_2_REC_INVOKEMETHOD(
266_1_test_InvokeMethod(
92_0_descend_Load(
x0),
x0),
x1,
x0) the following chains were created:
- We consider the chain 250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(220_0_descend_Return, x0[4]), x1[4], x0[4]) → 266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]), x1[4], x0[4]) which results in the following constraint:
(24) (250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(220_0_descend_Return, x0[4]), x1[4], x0[4])≥NonInfC∧250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(220_0_descend_Return, x0[4]), x1[4], x0[4])≥266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]), x1[4], x0[4])∧(UIncreasing(266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]), x1[4], x0[4])), ≥))
We simplified constraint (24) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(25) ((UIncreasing(266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]), x1[4], x0[4])), ≥)∧[(-1)bso_84] ≥ 0)
We simplified constraint (25) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(26) ((UIncreasing(266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]), x1[4], x0[4])), ≥)∧[(-1)bso_84] ≥ 0)
We simplified constraint (26) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(27) ((UIncreasing(266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]), x1[4], x0[4])), ≥)∧[(-1)bso_84] ≥ 0)
We simplified constraint (27) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(28) ((UIncreasing(266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]), x1[4], x0[4])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_84] ≥ 0)
For Pair
266_2_REC_INVOKEMETHOD(
266_1_test_InvokeMethod(
220_0_descend_Return,
x0),
x1,
x0) →
282_2_REC_INVOKEMETHOD(
282_1_test_InvokeMethod(
92_0_descend_Load(
x0),
x0),
x1,
x0) the following chains were created:
- We consider the chain 266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(220_0_descend_Return, x0[5]), x1[5], x0[5]) → 282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]), x1[5], x0[5]) which results in the following constraint:
(29) (266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(220_0_descend_Return, x0[5]), x1[5], x0[5])≥NonInfC∧266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(220_0_descend_Return, x0[5]), x1[5], x0[5])≥282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]), x1[5], x0[5])∧(UIncreasing(282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]), x1[5], x0[5])), ≥))
We simplified constraint (29) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(30) ((UIncreasing(282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]), x1[5], x0[5])), ≥)∧[(-1)bso_86] ≥ 0)
We simplified constraint (30) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(31) ((UIncreasing(282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]), x1[5], x0[5])), ≥)∧[(-1)bso_86] ≥ 0)
We simplified constraint (31) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(32) ((UIncreasing(282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]), x1[5], x0[5])), ≥)∧[(-1)bso_86] ≥ 0)
We simplified constraint (32) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(33) ((UIncreasing(282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]), x1[5], x0[5])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_86] ≥ 0)
For Pair
282_2_REC_INVOKEMETHOD(
282_1_test_InvokeMethod(
220_0_descend_Return,
x0),
x1,
x0) →
295_2_REC_INVOKEMETHOD(
295_1_test_InvokeMethod(
92_0_descend_Load(
x0),
x0),
x1,
x0) the following chains were created:
- We consider the chain 282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(220_0_descend_Return, x0[6]), x1[6], x0[6]) → 295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]), x1[6], x0[6]) which results in the following constraint:
(34) (282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(220_0_descend_Return, x0[6]), x1[6], x0[6])≥NonInfC∧282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(220_0_descend_Return, x0[6]), x1[6], x0[6])≥295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]), x1[6], x0[6])∧(UIncreasing(295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]), x1[6], x0[6])), ≥))
We simplified constraint (34) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(35) ((UIncreasing(295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]), x1[6], x0[6])), ≥)∧[(-1)bso_88] ≥ 0)
We simplified constraint (35) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(36) ((UIncreasing(295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]), x1[6], x0[6])), ≥)∧[(-1)bso_88] ≥ 0)
We simplified constraint (36) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(37) ((UIncreasing(295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]), x1[6], x0[6])), ≥)∧[(-1)bso_88] ≥ 0)
We simplified constraint (37) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(38) ((UIncreasing(295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]), x1[6], x0[6])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_88] ≥ 0)
For Pair
295_2_REC_INVOKEMETHOD(
295_1_test_InvokeMethod(
220_0_descend_Return,
x0),
x1,
x0) →
309_2_REC_INVOKEMETHOD(
309_1_test_InvokeMethod(
92_0_descend_Load(
x0),
x0),
x1,
x0) the following chains were created:
- We consider the chain 295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(220_0_descend_Return, x0[7]), x1[7], x0[7]) → 309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]), x1[7], x0[7]) which results in the following constraint:
(39) (295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(220_0_descend_Return, x0[7]), x1[7], x0[7])≥NonInfC∧295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(220_0_descend_Return, x0[7]), x1[7], x0[7])≥309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]), x1[7], x0[7])∧(UIncreasing(309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]), x1[7], x0[7])), ≥))
We simplified constraint (39) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(40) ((UIncreasing(309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]), x1[7], x0[7])), ≥)∧[(-1)bso_90] ≥ 0)
We simplified constraint (40) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(41) ((UIncreasing(309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]), x1[7], x0[7])), ≥)∧[(-1)bso_90] ≥ 0)
We simplified constraint (41) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(42) ((UIncreasing(309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]), x1[7], x0[7])), ≥)∧[(-1)bso_90] ≥ 0)
We simplified constraint (42) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(43) ((UIncreasing(309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]), x1[7], x0[7])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_90] ≥ 0)
For Pair
309_2_REC_INVOKEMETHOD(
309_1_test_InvokeMethod(
220_0_descend_Return,
x0),
x1,
x0) →
321_2_REC_INVOKEMETHOD(
321_1_test_InvokeMethod(
92_0_descend_Load(
x0),
x0),
x1,
x0) the following chains were created:
- We consider the chain 309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(220_0_descend_Return, x0[8]), x1[8], x0[8]) → 321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]), x1[8], x0[8]) which results in the following constraint:
(44) (309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(220_0_descend_Return, x0[8]), x1[8], x0[8])≥NonInfC∧309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(220_0_descend_Return, x0[8]), x1[8], x0[8])≥321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]), x1[8], x0[8])∧(UIncreasing(321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]), x1[8], x0[8])), ≥))
We simplified constraint (44) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(45) ((UIncreasing(321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]), x1[8], x0[8])), ≥)∧[(-1)bso_92] ≥ 0)
We simplified constraint (45) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(46) ((UIncreasing(321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]), x1[8], x0[8])), ≥)∧[(-1)bso_92] ≥ 0)
We simplified constraint (46) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(47) ((UIncreasing(321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]), x1[8], x0[8])), ≥)∧[(-1)bso_92] ≥ 0)
We simplified constraint (47) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(48) ((UIncreasing(321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]), x1[8], x0[8])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_92] ≥ 0)
For Pair
321_2_REC_INVOKEMETHOD(
321_1_test_InvokeMethod(
220_0_descend_Return,
x0),
x1,
x0) →
COND_321_2_REC_INVOKEMETHOD(
>(
x0,
0),
321_1_test_InvokeMethod(
220_0_descend_Return,
x0),
x1,
x0) the following chains were created:
- We consider the chain 321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9]) → COND_321_2_REC_INVOKEMETHOD(>(x0[9], 0), 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9]), COND_321_2_REC_INVOKEMETHOD(TRUE, 321_1_test_InvokeMethod(220_0_descend_Return, x0[10]), x1[10], x0[10]) → 69_0_REC_GE(x1[10], +(x0[10], 1)) which results in the following constraint:
(49) (>(x0[9], 0)=TRUE∧321_1_test_InvokeMethod(220_0_descend_Return, x0[9])=321_1_test_InvokeMethod(220_0_descend_Return, x0[10])∧x1[9]=x1[10]∧x0[9]=x0[10] ⇒ 321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])≥NonInfC∧321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])≥COND_321_2_REC_INVOKEMETHOD(>(x0[9], 0), 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])∧(UIncreasing(COND_321_2_REC_INVOKEMETHOD(>(x0[9], 0), 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])), ≥))
We simplified constraint (49) using rules (I), (II), (IV), (DELETE_TRIVIAL_REDUCESTO) which results in the following new constraint:
(50) (>(x0[9], 0)=TRUE ⇒ 321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])≥NonInfC∧321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])≥COND_321_2_REC_INVOKEMETHOD(>(x0[9], 0), 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])∧(UIncreasing(COND_321_2_REC_INVOKEMETHOD(>(x0[9], 0), 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])), ≥))
We simplified constraint (50) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(51) (x0[9] + [-1] ≥ 0 ⇒ (UIncreasing(COND_321_2_REC_INVOKEMETHOD(>(x0[9], 0), 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])), ≥)∧[(-1)bni_93 + (-1)Bound*bni_93] + [(2)bni_93]x1[9] ≥ 0∧[(-1)bso_94] ≥ 0)
We simplified constraint (51) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(52) (x0[9] + [-1] ≥ 0 ⇒ (UIncreasing(COND_321_2_REC_INVOKEMETHOD(>(x0[9], 0), 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])), ≥)∧[(-1)bni_93 + (-1)Bound*bni_93] + [(2)bni_93]x1[9] ≥ 0∧[(-1)bso_94] ≥ 0)
We simplified constraint (52) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(53) (x0[9] + [-1] ≥ 0 ⇒ (UIncreasing(COND_321_2_REC_INVOKEMETHOD(>(x0[9], 0), 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])), ≥)∧[(-1)bni_93 + (-1)Bound*bni_93] + [(2)bni_93]x1[9] ≥ 0∧[(-1)bso_94] ≥ 0)
We simplified constraint (53) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(54) (x0[9] + [-1] ≥ 0 ⇒ (UIncreasing(COND_321_2_REC_INVOKEMETHOD(>(x0[9], 0), 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])), ≥)∧[(2)bni_93] = 0∧[(-1)bni_93 + (-1)Bound*bni_93] ≥ 0∧0 = 0∧[(-1)bso_94] ≥ 0)
We simplified constraint (54) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(55) (x0[9] ≥ 0 ⇒ (UIncreasing(COND_321_2_REC_INVOKEMETHOD(>(x0[9], 0), 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])), ≥)∧[(2)bni_93] = 0∧[(-1)bni_93 + (-1)Bound*bni_93] ≥ 0∧0 = 0∧[(-1)bso_94] ≥ 0)
For Pair
COND_321_2_REC_INVOKEMETHOD(
TRUE,
321_1_test_InvokeMethod(
220_0_descend_Return,
x0),
x1,
x0) →
69_0_REC_GE(
x1,
+(
x0,
1)) the following chains were created:
- We consider the chain COND_321_2_REC_INVOKEMETHOD(TRUE, 321_1_test_InvokeMethod(220_0_descend_Return, x0[10]), x1[10], x0[10]) → 69_0_REC_GE(x1[10], +(x0[10], 1)) which results in the following constraint:
(56) (COND_321_2_REC_INVOKEMETHOD(TRUE, 321_1_test_InvokeMethod(220_0_descend_Return, x0[10]), x1[10], x0[10])≥NonInfC∧COND_321_2_REC_INVOKEMETHOD(TRUE, 321_1_test_InvokeMethod(220_0_descend_Return, x0[10]), x1[10], x0[10])≥69_0_REC_GE(x1[10], +(x0[10], 1))∧(UIncreasing(69_0_REC_GE(x1[10], +(x0[10], 1))), ≥))
We simplified constraint (56) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(57) ((UIncreasing(69_0_REC_GE(x1[10], +(x0[10], 1))), ≥)∧[(-1)bso_96] ≥ 0)
We simplified constraint (57) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(58) ((UIncreasing(69_0_REC_GE(x1[10], +(x0[10], 1))), ≥)∧[(-1)bso_96] ≥ 0)
We simplified constraint (58) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(59) ((UIncreasing(69_0_REC_GE(x1[10], +(x0[10], 1))), ≥)∧[(-1)bso_96] ≥ 0)
We simplified constraint (59) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(60) ((UIncreasing(69_0_REC_GE(x1[10], +(x0[10], 1))), ≥)∧0 = 0∧0 = 0∧[(-1)bso_96] ≥ 0)
For Pair
69_0_REC_GE(
x0,
x1) →
COND_69_0_REC_GE1(
&&(
&&(
&&(
>=(
x1,
100),
>(
x0,
0)),
>(
1,
0)),
<(
0,
-(
x0,
1))),
x0,
x1) the following chains were created:
- We consider the chain 69_0_REC_GE(x0[11], x1[11]) → COND_69_0_REC_GE1(&&(&&(&&(>=(x1[11], 100), >(x0[11], 0)), >(1, 0)), <(0, -(x0[11], 1))), x0[11], x1[11]), COND_69_0_REC_GE1(TRUE, x0[12], x1[12]) → 69_0_REC_GE(-(x0[12], 1), -(x0[12], 1)) which results in the following constraint:
(61) (&&(&&(&&(>=(x1[11], 100), >(x0[11], 0)), >(1, 0)), <(0, -(x0[11], 1)))=TRUE∧x0[11]=x0[12]∧x1[11]=x1[12] ⇒ 69_0_REC_GE(x0[11], x1[11])≥NonInfC∧69_0_REC_GE(x0[11], x1[11])≥COND_69_0_REC_GE1(&&(&&(&&(>=(x1[11], 100), >(x0[11], 0)), >(1, 0)), <(0, -(x0[11], 1))), x0[11], x1[11])∧(UIncreasing(COND_69_0_REC_GE1(&&(&&(&&(>=(x1[11], 100), >(x0[11], 0)), >(1, 0)), <(0, -(x0[11], 1))), x0[11], x1[11])), ≥))
We simplified constraint (61) using rules (IV), (IDP_CONSTANT_FOLD), (DELETE_TRIVIAL_REDUCESTO), (IDP_BOOLEAN) which results in the following new constraint:
(62) (<(0, -(x0[11], 1))=TRUE∧>=(x1[11], 100)=TRUE∧>(x0[11], 0)=TRUE ⇒ 69_0_REC_GE(x0[11], x1[11])≥NonInfC∧69_0_REC_GE(x0[11], x1[11])≥COND_69_0_REC_GE1(&&(&&(&&(>=(x1[11], 100), >(x0[11], 0)), >(1, 0)), <(0, -(x0[11], 1))), x0[11], x1[11])∧(UIncreasing(COND_69_0_REC_GE1(&&(&&(&&(>=(x1[11], 100), >(x0[11], 0)), >(1, 0)), <(0, -(x0[11], 1))), x0[11], x1[11])), ≥))
We simplified constraint (62) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(63) (x0[11] + [-2] ≥ 0∧x1[11] + [-100] ≥ 0∧x0[11] + [-1] ≥ 0 ⇒ (UIncreasing(COND_69_0_REC_GE1(&&(&&(&&(>=(x1[11], 100), >(x0[11], 0)), >(1, 0)), <(0, -(x0[11], 1))), x0[11], x1[11])), ≥)∧[(-1)bni_97 + (-1)Bound*bni_97] + [(2)bni_97]x0[11] ≥ 0∧[(-1)bso_98] ≥ 0)
We simplified constraint (63) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(64) (x0[11] + [-2] ≥ 0∧x1[11] + [-100] ≥ 0∧x0[11] + [-1] ≥ 0 ⇒ (UIncreasing(COND_69_0_REC_GE1(&&(&&(&&(>=(x1[11], 100), >(x0[11], 0)), >(1, 0)), <(0, -(x0[11], 1))), x0[11], x1[11])), ≥)∧[(-1)bni_97 + (-1)Bound*bni_97] + [(2)bni_97]x0[11] ≥ 0∧[(-1)bso_98] ≥ 0)
We simplified constraint (64) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(65) (x0[11] + [-2] ≥ 0∧x1[11] + [-100] ≥ 0∧x0[11] + [-1] ≥ 0 ⇒ (UIncreasing(COND_69_0_REC_GE1(&&(&&(&&(>=(x1[11], 100), >(x0[11], 0)), >(1, 0)), <(0, -(x0[11], 1))), x0[11], x1[11])), ≥)∧[(-1)bni_97 + (-1)Bound*bni_97] + [(2)bni_97]x0[11] ≥ 0∧[(-1)bso_98] ≥ 0)
We simplified constraint (65) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(66) (x0[11] ≥ 0∧x1[11] + [-100] ≥ 0∧[1] + x0[11] ≥ 0 ⇒ (UIncreasing(COND_69_0_REC_GE1(&&(&&(&&(>=(x1[11], 100), >(x0[11], 0)), >(1, 0)), <(0, -(x0[11], 1))), x0[11], x1[11])), ≥)∧[(3)bni_97 + (-1)Bound*bni_97] + [(2)bni_97]x0[11] ≥ 0∧[(-1)bso_98] ≥ 0)
We simplified constraint (66) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(67) (x0[11] ≥ 0∧x1[11] ≥ 0∧[1] + x0[11] ≥ 0 ⇒ (UIncreasing(COND_69_0_REC_GE1(&&(&&(&&(>=(x1[11], 100), >(x0[11], 0)), >(1, 0)), <(0, -(x0[11], 1))), x0[11], x1[11])), ≥)∧[(3)bni_97 + (-1)Bound*bni_97] + [(2)bni_97]x0[11] ≥ 0∧[(-1)bso_98] ≥ 0)
For Pair
COND_69_0_REC_GE1(
TRUE,
x0,
x1) →
69_0_REC_GE(
-(
x0,
1),
-(
x0,
1)) the following chains were created:
- We consider the chain COND_69_0_REC_GE1(TRUE, x0[12], x1[12]) → 69_0_REC_GE(-(x0[12], 1), -(x0[12], 1)) which results in the following constraint:
(68) (COND_69_0_REC_GE1(TRUE, x0[12], x1[12])≥NonInfC∧COND_69_0_REC_GE1(TRUE, x0[12], x1[12])≥69_0_REC_GE(-(x0[12], 1), -(x0[12], 1))∧(UIncreasing(69_0_REC_GE(-(x0[12], 1), -(x0[12], 1))), ≥))
We simplified constraint (68) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(69) ((UIncreasing(69_0_REC_GE(-(x0[12], 1), -(x0[12], 1))), ≥)∧[2 + (-1)bso_100] ≥ 0)
We simplified constraint (69) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(70) ((UIncreasing(69_0_REC_GE(-(x0[12], 1), -(x0[12], 1))), ≥)∧[2 + (-1)bso_100] ≥ 0)
We simplified constraint (70) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(71) ((UIncreasing(69_0_REC_GE(-(x0[12], 1), -(x0[12], 1))), ≥)∧[2 + (-1)bso_100] ≥ 0)
We simplified constraint (71) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(72) ((UIncreasing(69_0_REC_GE(-(x0[12], 1), -(x0[12], 1))), ≥)∧0 = 0∧0 = 0∧[2 + (-1)bso_100] ≥ 0)
To summarize, we get the following constraints P
≥ for the following pairs.
- 69_0_REC_GE(x0, x1) → COND_69_0_REC_GE(<(x1, 100), x0, x1)
- ([99] + x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(2)bni_75] = 0∧[(-1)bni_75 + (-1)Bound*bni_75] ≥ 0∧0 = 0∧[(-1)bso_76] ≥ 0)
- ([99] + [-1]x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(2)bni_75] = 0∧[(-1)bni_75 + (-1)Bound*bni_75] ≥ 0∧0 = 0∧[(-1)bso_76] ≥ 0)
- COND_69_0_REC_GE(TRUE, x0, x1) → 92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(92_0_descend_Load(x1), x1), x0, x1)
- ((UIncreasing(92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]), x0[1], x1[1])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_78] ≥ 0)
- 92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(220_0_descend_Return, x0), x1, x0) → 237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(92_0_descend_Load(x0), x0), x1, x0)
- ((UIncreasing(237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(92_0_descend_Load(x0[2]), x0[2]), x1[2], x0[2])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_80] ≥ 0)
- 237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(220_0_descend_Return, x0), x1, x0) → 250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(92_0_descend_Load(x0), x0), x1, x0)
- ((UIncreasing(250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]), x1[3], x0[3])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_82] ≥ 0)
- 250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(220_0_descend_Return, x0), x1, x0) → 266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(92_0_descend_Load(x0), x0), x1, x0)
- ((UIncreasing(266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]), x1[4], x0[4])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_84] ≥ 0)
- 266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(220_0_descend_Return, x0), x1, x0) → 282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(92_0_descend_Load(x0), x0), x1, x0)
- ((UIncreasing(282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]), x1[5], x0[5])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_86] ≥ 0)
- 282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(220_0_descend_Return, x0), x1, x0) → 295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(92_0_descend_Load(x0), x0), x1, x0)
- ((UIncreasing(295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]), x1[6], x0[6])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_88] ≥ 0)
- 295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(220_0_descend_Return, x0), x1, x0) → 309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(92_0_descend_Load(x0), x0), x1, x0)
- ((UIncreasing(309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]), x1[7], x0[7])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_90] ≥ 0)
- 309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(220_0_descend_Return, x0), x1, x0) → 321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(92_0_descend_Load(x0), x0), x1, x0)
- ((UIncreasing(321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]), x1[8], x0[8])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_92] ≥ 0)
- 321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(220_0_descend_Return, x0), x1, x0) → COND_321_2_REC_INVOKEMETHOD(>(x0, 0), 321_1_test_InvokeMethod(220_0_descend_Return, x0), x1, x0)
- (x0[9] ≥ 0 ⇒ (UIncreasing(COND_321_2_REC_INVOKEMETHOD(>(x0[9], 0), 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])), ≥)∧[(2)bni_93] = 0∧[(-1)bni_93 + (-1)Bound*bni_93] ≥ 0∧0 = 0∧[(-1)bso_94] ≥ 0)
- COND_321_2_REC_INVOKEMETHOD(TRUE, 321_1_test_InvokeMethod(220_0_descend_Return, x0), x1, x0) → 69_0_REC_GE(x1, +(x0, 1))
- ((UIncreasing(69_0_REC_GE(x1[10], +(x0[10], 1))), ≥)∧0 = 0∧0 = 0∧[(-1)bso_96] ≥ 0)
- 69_0_REC_GE(x0, x1) → COND_69_0_REC_GE1(&&(&&(&&(>=(x1, 100), >(x0, 0)), >(1, 0)), <(0, -(x0, 1))), x0, x1)
- (x0[11] ≥ 0∧x1[11] ≥ 0∧[1] + x0[11] ≥ 0 ⇒ (UIncreasing(COND_69_0_REC_GE1(&&(&&(&&(>=(x1[11], 100), >(x0[11], 0)), >(1, 0)), <(0, -(x0[11], 1))), x0[11], x1[11])), ≥)∧[(3)bni_97 + (-1)Bound*bni_97] + [(2)bni_97]x0[11] ≥ 0∧[(-1)bso_98] ≥ 0)
- COND_69_0_REC_GE1(TRUE, x0, x1) → 69_0_REC_GE(-(x0, 1), -(x0, 1))
- ((UIncreasing(69_0_REC_GE(-(x0[12], 1), -(x0[12], 1))), ≥)∧0 = 0∧0 = 0∧[2 + (-1)bso_100] ≥ 0)
The constraints for P
> respective P
bound are constructed from P
≥ where we just replace every occurence of "t ≥ s" in P
≥ by "t > s" respective "t ≥
c". Here
c stands for the fresh constant used for P
bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:
POL(TRUE) = 0
POL(FALSE) = 0
POL(92_0_descend_Load(x1)) = [-1]
POL(181_0_descend_Return) = [-1]
POL(243_0_descend_Return) = [-1]
POL(256_0_descend_Return) = [-1]
POL(273_0_descend_Return) = [-1]
POL(287_0_descend_Return) = [-1]
POL(300_0_descend_Return) = [-1]
POL(314_0_descend_Return) = [-1]
POL(327_0_descend_Return) = [-1]
POL(169_0_descend_LE(x1)) = [-1]
POL(97_1_rec_InvokeMethod(x1, x2)) = [-1]
POL(47_0_rec_Return) = [-1]
POL(0) = 0
POL(143_0_rec_Return) = [-1]
POL(175_0_descend_Return) = [-1]
POL(Cond_169_0_descend_LE(x1, x2)) = [-1]
POL(>(x1, x2)) = [-1]
POL(191_1_descend_InvokeMethod(x1, x2)) = [-1]
POL(-(x1, x2)) = x1 + [-1]x2
POL(1) = [1]
POL(220_0_descend_Return) = [-1]
POL(69_0_REC_GE(x1, x2)) = [-1] + [2]x1
POL(COND_69_0_REC_GE(x1, x2, x3)) = [-1] + [2]x2
POL(<(x1, x2)) = [-1]
POL(100) = [100]
POL(92_2_REC_INVOKEMETHOD(x1, x2, x3)) = [-1] + [-1]x1 + [2]x2
POL(92_1_test_InvokeMethod(x1, x2)) = [-1] + [-1]x1
POL(237_2_REC_INVOKEMETHOD(x1, x2, x3)) = [-1] + [-1]x1 + [2]x2
POL(237_1_test_InvokeMethod(x1, x2)) = [-1] + [-1]x1
POL(250_2_REC_INVOKEMETHOD(x1, x2, x3)) = [-1] + [-1]x1 + [2]x2
POL(250_1_test_InvokeMethod(x1, x2)) = [-1] + [-1]x1
POL(266_2_REC_INVOKEMETHOD(x1, x2, x3)) = [-1] + [2]x2
POL(266_1_test_InvokeMethod(x1, x2)) = [-1] + [-1]x2 + [-1]x1
POL(282_2_REC_INVOKEMETHOD(x1, x2, x3)) = [-1] + [-1]x1 + [2]x2
POL(282_1_test_InvokeMethod(x1, x2)) = [-1] + [-1]x1
POL(295_2_REC_INVOKEMETHOD(x1, x2, x3)) = [-1] + [2]x2
POL(295_1_test_InvokeMethod(x1, x2)) = [-1] + [-1]x2 + [-1]x1
POL(309_2_REC_INVOKEMETHOD(x1, x2, x3)) = [-1] + [-1]x1 + [2]x2
POL(309_1_test_InvokeMethod(x1, x2)) = [-1] + [-1]x1
POL(321_2_REC_INVOKEMETHOD(x1, x2, x3)) = [-1] + x1 + [2]x2
POL(321_1_test_InvokeMethod(x1, x2)) = [-1] + [-1]x1
POL(COND_321_2_REC_INVOKEMETHOD(x1, x2, x3, x4)) = [-1] + [2]x3 + x2
POL(+(x1, x2)) = x1 + x2
POL(COND_69_0_REC_GE1(x1, x2, x3)) = [-1] + [2]x2
POL(&&(x1, x2)) = [-1]
POL(>=(x1, x2)) = [-1]
The following pairs are in P
>:
COND_69_0_REC_GE1(TRUE, x0[12], x1[12]) → 69_0_REC_GE(-(x0[12], 1), -(x0[12], 1))
The following pairs are in P
bound:
69_0_REC_GE(x0[11], x1[11]) → COND_69_0_REC_GE1(&&(&&(&&(>=(x1[11], 100), >(x0[11], 0)), >(1, 0)), <(0, -(x0[11], 1))), x0[11], x1[11])
The following pairs are in P
≥:
69_0_REC_GE(x0[0], x1[0]) → COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])
COND_69_0_REC_GE(TRUE, x0[1], x1[1]) → 92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]), x0[1], x1[1])
92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(220_0_descend_Return, x0[2]), x1[2], x0[2]) → 237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(92_0_descend_Load(x0[2]), x0[2]), x1[2], x0[2])
237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(220_0_descend_Return, x0[3]), x1[3], x0[3]) → 250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]), x1[3], x0[3])
250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(220_0_descend_Return, x0[4]), x1[4], x0[4]) → 266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]), x1[4], x0[4])
266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(220_0_descend_Return, x0[5]), x1[5], x0[5]) → 282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]), x1[5], x0[5])
282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(220_0_descend_Return, x0[6]), x1[6], x0[6]) → 295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]), x1[6], x0[6])
295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(220_0_descend_Return, x0[7]), x1[7], x0[7]) → 309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]), x1[7], x0[7])
309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(220_0_descend_Return, x0[8]), x1[8], x0[8]) → 321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]), x1[8], x0[8])
321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9]) → COND_321_2_REC_INVOKEMETHOD(>(x0[9], 0), 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])
COND_321_2_REC_INVOKEMETHOD(TRUE, 321_1_test_InvokeMethod(220_0_descend_Return, x0[10]), x1[10], x0[10]) → 69_0_REC_GE(x1[10], +(x0[10], 1))
69_0_REC_GE(x0[11], x1[11]) → COND_69_0_REC_GE1(&&(&&(&&(>=(x1[11], 100), >(x0[11], 0)), >(1, 0)), <(0, -(x0[11], 1))), x0[11], x1[11])
At least the following rules have been oriented under context sensitive arithmetic replacement:
92_0_descend_Load(i12)1 ↔ 181_0_descend_Return1
92_0_descend_Load(i45)1 ↔ 243_0_descend_Return1
92_0_descend_Load(i59)1 ↔ 256_0_descend_Return1
92_0_descend_Load(i62)1 ↔ 273_0_descend_Return1
92_0_descend_Load(i67)1 ↔ 287_0_descend_Return1
92_0_descend_Load(i70)1 ↔ 300_0_descend_Return1
92_0_descend_Load(i74)1 ↔ 314_0_descend_Return1
92_0_descend_Load(i76)1 ↔ 327_0_descend_Return1
92_0_descend_Load(x0)1 ↔ 169_0_descend_LE(x0)1
169_0_descend_LE(0)1 ↔ 175_0_descend_Return1
169_0_descend_LE(x0)1 ↔ Cond_169_0_descend_LE(>(x0, 0), x0)1
Cond_169_0_descend_LE(TRUE, x0)1 ↔ 191_1_descend_InvokeMethod(169_0_descend_LE(-(x0, 1)), -(x0, 1))1
191_1_descend_InvokeMethod(175_0_descend_Return, 0)1 ↔ 220_0_descend_Return1
191_1_descend_InvokeMethod(220_0_descend_Return, x0)1 ↔ 220_0_descend_Return1
(16) Complex Obligation (AND)
(17) Obligation:
IDP problem:
The following function symbols are pre-defined:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
| ~ | Bwxor: (Integer, Integer) -> Integer |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
The following domains are used:
Integer, Boolean
The ITRS R consists of the following rules:
92_0_descend_Load(
i12) →
181_0_descend_Return92_0_descend_Load(
i45) →
243_0_descend_Return92_0_descend_Load(
i59) →
256_0_descend_Return92_0_descend_Load(
i62) →
273_0_descend_Return92_0_descend_Load(
i67) →
287_0_descend_Return92_0_descend_Load(
i70) →
300_0_descend_Return92_0_descend_Load(
i74) →
314_0_descend_Return92_0_descend_Load(
i76) →
327_0_descend_Return92_0_descend_Load(
x0) →
169_0_descend_LE(
x0)
97_1_rec_InvokeMethod(
47_0_rec_Return,
0) →
143_0_rec_Return97_1_rec_InvokeMethod(
143_0_rec_Return,
x0) →
143_0_rec_Return169_0_descend_LE(
0) →
175_0_descend_Return169_0_descend_LE(
x0) →
Cond_169_0_descend_LE(
x0 > 0,
x0)
Cond_169_0_descend_LE(
TRUE,
x0) →
191_1_descend_InvokeMethod(
169_0_descend_LE(
x0 - 1),
x0 - 1)
191_1_descend_InvokeMethod(
175_0_descend_Return,
0) →
220_0_descend_Return191_1_descend_InvokeMethod(
220_0_descend_Return,
x0) →
220_0_descend_ReturnThe integer pair graph contains the following rules and edges:
(0):
69_0_REC_GE(
x0[0],
x1[0]) →
COND_69_0_REC_GE(
x1[0] < 100,
x0[0],
x1[0])
(1):
COND_69_0_REC_GE(
TRUE,
x0[1],
x1[1]) →
92_2_REC_INVOKEMETHOD(
92_1_test_InvokeMethod(
92_0_descend_Load(
x1[1]),
x1[1]),
x0[1],
x1[1])
(2):
92_2_REC_INVOKEMETHOD(
92_1_test_InvokeMethod(
220_0_descend_Return,
x0[2]),
x1[2],
x0[2]) →
237_2_REC_INVOKEMETHOD(
237_1_test_InvokeMethod(
92_0_descend_Load(
x0[2]),
x0[2]),
x1[2],
x0[2])
(3):
237_2_REC_INVOKEMETHOD(
237_1_test_InvokeMethod(
220_0_descend_Return,
x0[3]),
x1[3],
x0[3]) →
250_2_REC_INVOKEMETHOD(
250_1_test_InvokeMethod(
92_0_descend_Load(
x0[3]),
x0[3]),
x1[3],
x0[3])
(4):
250_2_REC_INVOKEMETHOD(
250_1_test_InvokeMethod(
220_0_descend_Return,
x0[4]),
x1[4],
x0[4]) →
266_2_REC_INVOKEMETHOD(
266_1_test_InvokeMethod(
92_0_descend_Load(
x0[4]),
x0[4]),
x1[4],
x0[4])
(5):
266_2_REC_INVOKEMETHOD(
266_1_test_InvokeMethod(
220_0_descend_Return,
x0[5]),
x1[5],
x0[5]) →
282_2_REC_INVOKEMETHOD(
282_1_test_InvokeMethod(
92_0_descend_Load(
x0[5]),
x0[5]),
x1[5],
x0[5])
(6):
282_2_REC_INVOKEMETHOD(
282_1_test_InvokeMethod(
220_0_descend_Return,
x0[6]),
x1[6],
x0[6]) →
295_2_REC_INVOKEMETHOD(
295_1_test_InvokeMethod(
92_0_descend_Load(
x0[6]),
x0[6]),
x1[6],
x0[6])
(7):
295_2_REC_INVOKEMETHOD(
295_1_test_InvokeMethod(
220_0_descend_Return,
x0[7]),
x1[7],
x0[7]) →
309_2_REC_INVOKEMETHOD(
309_1_test_InvokeMethod(
92_0_descend_Load(
x0[7]),
x0[7]),
x1[7],
x0[7])
(8):
309_2_REC_INVOKEMETHOD(
309_1_test_InvokeMethod(
220_0_descend_Return,
x0[8]),
x1[8],
x0[8]) →
321_2_REC_INVOKEMETHOD(
321_1_test_InvokeMethod(
92_0_descend_Load(
x0[8]),
x0[8]),
x1[8],
x0[8])
(9):
321_2_REC_INVOKEMETHOD(
321_1_test_InvokeMethod(
220_0_descend_Return,
x0[9]),
x1[9],
x0[9]) →
COND_321_2_REC_INVOKEMETHOD(
x0[9] > 0,
321_1_test_InvokeMethod(
220_0_descend_Return,
x0[9]),
x1[9],
x0[9])
(10):
COND_321_2_REC_INVOKEMETHOD(
TRUE,
321_1_test_InvokeMethod(
220_0_descend_Return,
x0[10]),
x1[10],
x0[10]) →
69_0_REC_GE(
x1[10],
x0[10] + 1)
(11):
69_0_REC_GE(
x0[11],
x1[11]) →
COND_69_0_REC_GE1(
x1[11] >= 100 && x0[11] > 0 && 1 > 0 && 0 < x0[11] - 1,
x0[11],
x1[11])
(10) -> (0), if ((x1[10] →* x0[0])∧(x0[10] + 1 →* x1[0]))
(0) -> (1), if ((x1[0] < 100 →* TRUE)∧(x0[0] →* x0[1])∧(x1[0] →* x1[1]))
(1) -> (2), if ((92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]) →* 92_1_test_InvokeMethod(220_0_descend_Return, x0[2]))∧(x0[1] →* x1[2])∧(x1[1] →* x0[2]))
(2) -> (3), if ((237_1_test_InvokeMethod(92_0_descend_Load(x0[2]), x0[2]) →* 237_1_test_InvokeMethod(220_0_descend_Return, x0[3]))∧(x1[2] →* x1[3])∧(x0[2] →* x0[3]))
(3) -> (4), if ((250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]) →* 250_1_test_InvokeMethod(220_0_descend_Return, x0[4]))∧(x1[3] →* x1[4])∧(x0[3] →* x0[4]))
(4) -> (5), if ((266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]) →* 266_1_test_InvokeMethod(220_0_descend_Return, x0[5]))∧(x1[4] →* x1[5])∧(x0[4] →* x0[5]))
(5) -> (6), if ((282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]) →* 282_1_test_InvokeMethod(220_0_descend_Return, x0[6]))∧(x1[5] →* x1[6])∧(x0[5] →* x0[6]))
(6) -> (7), if ((295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]) →* 295_1_test_InvokeMethod(220_0_descend_Return, x0[7]))∧(x1[6] →* x1[7])∧(x0[6] →* x0[7]))
(7) -> (8), if ((309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]) →* 309_1_test_InvokeMethod(220_0_descend_Return, x0[8]))∧(x1[7] →* x1[8])∧(x0[7] →* x0[8]))
(8) -> (9), if ((321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]) →* 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]))∧(x1[8] →* x1[9])∧(x0[8] →* x0[9]))
(9) -> (10), if ((x0[9] > 0 →* TRUE)∧(321_1_test_InvokeMethod(220_0_descend_Return, x0[9]) →* 321_1_test_InvokeMethod(220_0_descend_Return, x0[10]))∧(x1[9] →* x1[10])∧(x0[9] →* x0[10]))
(10) -> (11), if ((x1[10] →* x0[11])∧(x0[10] + 1 →* x1[11]))
The set Q consists of the following terms:
92_0_descend_Load(
x0)
97_1_rec_InvokeMethod(
47_0_rec_Return,
0)
97_1_rec_InvokeMethod(
143_0_rec_Return,
x0)
169_0_descend_LE(
x0)
Cond_169_0_descend_LE(
TRUE,
x0)
191_1_descend_InvokeMethod(
175_0_descend_Return,
0)
191_1_descend_InvokeMethod(
220_0_descend_Return,
x0)
(18) IDependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(19) Obligation:
IDP problem:
The following function symbols are pre-defined:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
| ~ | Bwxor: (Integer, Integer) -> Integer |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
The following domains are used:
Integer
The ITRS R consists of the following rules:
92_0_descend_Load(
i12) →
181_0_descend_Return92_0_descend_Load(
i45) →
243_0_descend_Return92_0_descend_Load(
i59) →
256_0_descend_Return92_0_descend_Load(
i62) →
273_0_descend_Return92_0_descend_Load(
i67) →
287_0_descend_Return92_0_descend_Load(
i70) →
300_0_descend_Return92_0_descend_Load(
i74) →
314_0_descend_Return92_0_descend_Load(
i76) →
327_0_descend_Return92_0_descend_Load(
x0) →
169_0_descend_LE(
x0)
97_1_rec_InvokeMethod(
47_0_rec_Return,
0) →
143_0_rec_Return97_1_rec_InvokeMethod(
143_0_rec_Return,
x0) →
143_0_rec_Return169_0_descend_LE(
0) →
175_0_descend_Return169_0_descend_LE(
x0) →
Cond_169_0_descend_LE(
x0 > 0,
x0)
Cond_169_0_descend_LE(
TRUE,
x0) →
191_1_descend_InvokeMethod(
169_0_descend_LE(
x0 - 1),
x0 - 1)
191_1_descend_InvokeMethod(
175_0_descend_Return,
0) →
220_0_descend_Return191_1_descend_InvokeMethod(
220_0_descend_Return,
x0) →
220_0_descend_ReturnThe integer pair graph contains the following rules and edges:
(10):
COND_321_2_REC_INVOKEMETHOD(
TRUE,
321_1_test_InvokeMethod(
220_0_descend_Return,
x0[10]),
x1[10],
x0[10]) →
69_0_REC_GE(
x1[10],
x0[10] + 1)
(9):
321_2_REC_INVOKEMETHOD(
321_1_test_InvokeMethod(
220_0_descend_Return,
x0[9]),
x1[9],
x0[9]) →
COND_321_2_REC_INVOKEMETHOD(
x0[9] > 0,
321_1_test_InvokeMethod(
220_0_descend_Return,
x0[9]),
x1[9],
x0[9])
(8):
309_2_REC_INVOKEMETHOD(
309_1_test_InvokeMethod(
220_0_descend_Return,
x0[8]),
x1[8],
x0[8]) →
321_2_REC_INVOKEMETHOD(
321_1_test_InvokeMethod(
92_0_descend_Load(
x0[8]),
x0[8]),
x1[8],
x0[8])
(7):
295_2_REC_INVOKEMETHOD(
295_1_test_InvokeMethod(
220_0_descend_Return,
x0[7]),
x1[7],
x0[7]) →
309_2_REC_INVOKEMETHOD(
309_1_test_InvokeMethod(
92_0_descend_Load(
x0[7]),
x0[7]),
x1[7],
x0[7])
(6):
282_2_REC_INVOKEMETHOD(
282_1_test_InvokeMethod(
220_0_descend_Return,
x0[6]),
x1[6],
x0[6]) →
295_2_REC_INVOKEMETHOD(
295_1_test_InvokeMethod(
92_0_descend_Load(
x0[6]),
x0[6]),
x1[6],
x0[6])
(5):
266_2_REC_INVOKEMETHOD(
266_1_test_InvokeMethod(
220_0_descend_Return,
x0[5]),
x1[5],
x0[5]) →
282_2_REC_INVOKEMETHOD(
282_1_test_InvokeMethod(
92_0_descend_Load(
x0[5]),
x0[5]),
x1[5],
x0[5])
(4):
250_2_REC_INVOKEMETHOD(
250_1_test_InvokeMethod(
220_0_descend_Return,
x0[4]),
x1[4],
x0[4]) →
266_2_REC_INVOKEMETHOD(
266_1_test_InvokeMethod(
92_0_descend_Load(
x0[4]),
x0[4]),
x1[4],
x0[4])
(3):
237_2_REC_INVOKEMETHOD(
237_1_test_InvokeMethod(
220_0_descend_Return,
x0[3]),
x1[3],
x0[3]) →
250_2_REC_INVOKEMETHOD(
250_1_test_InvokeMethod(
92_0_descend_Load(
x0[3]),
x0[3]),
x1[3],
x0[3])
(2):
92_2_REC_INVOKEMETHOD(
92_1_test_InvokeMethod(
220_0_descend_Return,
x0[2]),
x1[2],
x0[2]) →
237_2_REC_INVOKEMETHOD(
237_1_test_InvokeMethod(
92_0_descend_Load(
x0[2]),
x0[2]),
x1[2],
x0[2])
(1):
COND_69_0_REC_GE(
TRUE,
x0[1],
x1[1]) →
92_2_REC_INVOKEMETHOD(
92_1_test_InvokeMethod(
92_0_descend_Load(
x1[1]),
x1[1]),
x0[1],
x1[1])
(0):
69_0_REC_GE(
x0[0],
x1[0]) →
COND_69_0_REC_GE(
x1[0] < 100,
x0[0],
x1[0])
(10) -> (0), if ((x1[10] →* x0[0])∧(x0[10] + 1 →* x1[0]))
(0) -> (1), if ((x1[0] < 100 →* TRUE)∧(x0[0] →* x0[1])∧(x1[0] →* x1[1]))
(1) -> (2), if ((92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]) →* 92_1_test_InvokeMethod(220_0_descend_Return, x0[2]))∧(x0[1] →* x1[2])∧(x1[1] →* x0[2]))
(2) -> (3), if ((237_1_test_InvokeMethod(92_0_descend_Load(x0[2]), x0[2]) →* 237_1_test_InvokeMethod(220_0_descend_Return, x0[3]))∧(x1[2] →* x1[3])∧(x0[2] →* x0[3]))
(3) -> (4), if ((250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]) →* 250_1_test_InvokeMethod(220_0_descend_Return, x0[4]))∧(x1[3] →* x1[4])∧(x0[3] →* x0[4]))
(4) -> (5), if ((266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]) →* 266_1_test_InvokeMethod(220_0_descend_Return, x0[5]))∧(x1[4] →* x1[5])∧(x0[4] →* x0[5]))
(5) -> (6), if ((282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]) →* 282_1_test_InvokeMethod(220_0_descend_Return, x0[6]))∧(x1[5] →* x1[6])∧(x0[5] →* x0[6]))
(6) -> (7), if ((295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]) →* 295_1_test_InvokeMethod(220_0_descend_Return, x0[7]))∧(x1[6] →* x1[7])∧(x0[6] →* x0[7]))
(7) -> (8), if ((309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]) →* 309_1_test_InvokeMethod(220_0_descend_Return, x0[8]))∧(x1[7] →* x1[8])∧(x0[7] →* x0[8]))
(8) -> (9), if ((321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]) →* 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]))∧(x1[8] →* x1[9])∧(x0[8] →* x0[9]))
(9) -> (10), if ((x0[9] > 0 →* TRUE)∧(321_1_test_InvokeMethod(220_0_descend_Return, x0[9]) →* 321_1_test_InvokeMethod(220_0_descend_Return, x0[10]))∧(x1[9] →* x1[10])∧(x0[9] →* x0[10]))
The set Q consists of the following terms:
92_0_descend_Load(
x0)
97_1_rec_InvokeMethod(
47_0_rec_Return,
0)
97_1_rec_InvokeMethod(
143_0_rec_Return,
x0)
169_0_descend_LE(
x0)
Cond_169_0_descend_LE(
TRUE,
x0)
191_1_descend_InvokeMethod(
175_0_descend_Return,
0)
191_1_descend_InvokeMethod(
220_0_descend_Return,
x0)
(20) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(21) Obligation:
IDP problem:
The following function symbols are pre-defined:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
| ~ | Bwxor: (Integer, Integer) -> Integer |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
The following domains are used:
Integer
The ITRS R consists of the following rules:
92_0_descend_Load(
i12) →
181_0_descend_Return92_0_descend_Load(
i45) →
243_0_descend_Return92_0_descend_Load(
i59) →
256_0_descend_Return92_0_descend_Load(
i62) →
273_0_descend_Return92_0_descend_Load(
i67) →
287_0_descend_Return92_0_descend_Load(
i70) →
300_0_descend_Return92_0_descend_Load(
i74) →
314_0_descend_Return92_0_descend_Load(
i76) →
327_0_descend_Return92_0_descend_Load(
x0) →
169_0_descend_LE(
x0)
169_0_descend_LE(
0) →
175_0_descend_Return169_0_descend_LE(
x0) →
Cond_169_0_descend_LE(
x0 > 0,
x0)
Cond_169_0_descend_LE(
TRUE,
x0) →
191_1_descend_InvokeMethod(
169_0_descend_LE(
x0 - 1),
x0 - 1)
191_1_descend_InvokeMethod(
175_0_descend_Return,
0) →
220_0_descend_Return191_1_descend_InvokeMethod(
220_0_descend_Return,
x0) →
220_0_descend_ReturnThe integer pair graph contains the following rules and edges:
(10):
COND_321_2_REC_INVOKEMETHOD(
TRUE,
321_1_test_InvokeMethod(
220_0_descend_Return,
x0[10]),
x1[10],
x0[10]) →
69_0_REC_GE(
x1[10],
x0[10] + 1)
(9):
321_2_REC_INVOKEMETHOD(
321_1_test_InvokeMethod(
220_0_descend_Return,
x0[9]),
x1[9],
x0[9]) →
COND_321_2_REC_INVOKEMETHOD(
x0[9] > 0,
321_1_test_InvokeMethod(
220_0_descend_Return,
x0[9]),
x1[9],
x0[9])
(8):
309_2_REC_INVOKEMETHOD(
309_1_test_InvokeMethod(
220_0_descend_Return,
x0[8]),
x1[8],
x0[8]) →
321_2_REC_INVOKEMETHOD(
321_1_test_InvokeMethod(
92_0_descend_Load(
x0[8]),
x0[8]),
x1[8],
x0[8])
(7):
295_2_REC_INVOKEMETHOD(
295_1_test_InvokeMethod(
220_0_descend_Return,
x0[7]),
x1[7],
x0[7]) →
309_2_REC_INVOKEMETHOD(
309_1_test_InvokeMethod(
92_0_descend_Load(
x0[7]),
x0[7]),
x1[7],
x0[7])
(6):
282_2_REC_INVOKEMETHOD(
282_1_test_InvokeMethod(
220_0_descend_Return,
x0[6]),
x1[6],
x0[6]) →
295_2_REC_INVOKEMETHOD(
295_1_test_InvokeMethod(
92_0_descend_Load(
x0[6]),
x0[6]),
x1[6],
x0[6])
(5):
266_2_REC_INVOKEMETHOD(
266_1_test_InvokeMethod(
220_0_descend_Return,
x0[5]),
x1[5],
x0[5]) →
282_2_REC_INVOKEMETHOD(
282_1_test_InvokeMethod(
92_0_descend_Load(
x0[5]),
x0[5]),
x1[5],
x0[5])
(4):
250_2_REC_INVOKEMETHOD(
250_1_test_InvokeMethod(
220_0_descend_Return,
x0[4]),
x1[4],
x0[4]) →
266_2_REC_INVOKEMETHOD(
266_1_test_InvokeMethod(
92_0_descend_Load(
x0[4]),
x0[4]),
x1[4],
x0[4])
(3):
237_2_REC_INVOKEMETHOD(
237_1_test_InvokeMethod(
220_0_descend_Return,
x0[3]),
x1[3],
x0[3]) →
250_2_REC_INVOKEMETHOD(
250_1_test_InvokeMethod(
92_0_descend_Load(
x0[3]),
x0[3]),
x1[3],
x0[3])
(2):
92_2_REC_INVOKEMETHOD(
92_1_test_InvokeMethod(
220_0_descend_Return,
x0[2]),
x1[2],
x0[2]) →
237_2_REC_INVOKEMETHOD(
237_1_test_InvokeMethod(
92_0_descend_Load(
x0[2]),
x0[2]),
x1[2],
x0[2])
(1):
COND_69_0_REC_GE(
TRUE,
x0[1],
x1[1]) →
92_2_REC_INVOKEMETHOD(
92_1_test_InvokeMethod(
92_0_descend_Load(
x1[1]),
x1[1]),
x0[1],
x1[1])
(0):
69_0_REC_GE(
x0[0],
x1[0]) →
COND_69_0_REC_GE(
x1[0] < 100,
x0[0],
x1[0])
(10) -> (0), if ((x1[10] →* x0[0])∧(x0[10] + 1 →* x1[0]))
(0) -> (1), if ((x1[0] < 100 →* TRUE)∧(x0[0] →* x0[1])∧(x1[0] →* x1[1]))
(1) -> (2), if ((92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]) →* 92_1_test_InvokeMethod(220_0_descend_Return, x0[2]))∧(x0[1] →* x1[2])∧(x1[1] →* x0[2]))
(2) -> (3), if ((237_1_test_InvokeMethod(92_0_descend_Load(x0[2]), x0[2]) →* 237_1_test_InvokeMethod(220_0_descend_Return, x0[3]))∧(x1[2] →* x1[3])∧(x0[2] →* x0[3]))
(3) -> (4), if ((250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]) →* 250_1_test_InvokeMethod(220_0_descend_Return, x0[4]))∧(x1[3] →* x1[4])∧(x0[3] →* x0[4]))
(4) -> (5), if ((266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]) →* 266_1_test_InvokeMethod(220_0_descend_Return, x0[5]))∧(x1[4] →* x1[5])∧(x0[4] →* x0[5]))
(5) -> (6), if ((282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]) →* 282_1_test_InvokeMethod(220_0_descend_Return, x0[6]))∧(x1[5] →* x1[6])∧(x0[5] →* x0[6]))
(6) -> (7), if ((295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]) →* 295_1_test_InvokeMethod(220_0_descend_Return, x0[7]))∧(x1[6] →* x1[7])∧(x0[6] →* x0[7]))
(7) -> (8), if ((309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]) →* 309_1_test_InvokeMethod(220_0_descend_Return, x0[8]))∧(x1[7] →* x1[8])∧(x0[7] →* x0[8]))
(8) -> (9), if ((321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]) →* 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]))∧(x1[8] →* x1[9])∧(x0[8] →* x0[9]))
(9) -> (10), if ((x0[9] > 0 →* TRUE)∧(321_1_test_InvokeMethod(220_0_descend_Return, x0[9]) →* 321_1_test_InvokeMethod(220_0_descend_Return, x0[10]))∧(x1[9] →* x1[10])∧(x0[9] →* x0[10]))
The set Q consists of the following terms:
92_0_descend_Load(
x0)
97_1_rec_InvokeMethod(
47_0_rec_Return,
0)
97_1_rec_InvokeMethod(
143_0_rec_Return,
x0)
169_0_descend_LE(
x0)
Cond_169_0_descend_LE(
TRUE,
x0)
191_1_descend_InvokeMethod(
175_0_descend_Return,
0)
191_1_descend_InvokeMethod(
220_0_descend_Return,
x0)
(22) IDPNonInfProof (SOUND transformation)
The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that
final constraints are written in
bold face.
For Pair
COND_321_2_REC_INVOKEMETHOD(
TRUE,
321_1_test_InvokeMethod(
220_0_descend_Return,
x0[10]),
x1[10],
x0[10]) →
69_0_REC_GE(
x1[10],
+(
x0[10],
1)) the following chains were created:
- We consider the chain COND_321_2_REC_INVOKEMETHOD(TRUE, 321_1_test_InvokeMethod(220_0_descend_Return, x0[10]), x1[10], x0[10]) → 69_0_REC_GE(x1[10], +(x0[10], 1)) which results in the following constraint:
(1) (COND_321_2_REC_INVOKEMETHOD(TRUE, 321_1_test_InvokeMethod(220_0_descend_Return, x0[10]), x1[10], x0[10])≥NonInfC∧COND_321_2_REC_INVOKEMETHOD(TRUE, 321_1_test_InvokeMethod(220_0_descend_Return, x0[10]), x1[10], x0[10])≥69_0_REC_GE(x1[10], +(x0[10], 1))∧(UIncreasing(69_0_REC_GE(x1[10], +(x0[10], 1))), ≥))
We simplified constraint (1) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(2) ((UIncreasing(69_0_REC_GE(x1[10], +(x0[10], 1))), ≥)∧[(-1)bso_40] ≥ 0)
We simplified constraint (2) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(3) ((UIncreasing(69_0_REC_GE(x1[10], +(x0[10], 1))), ≥)∧[(-1)bso_40] ≥ 0)
We simplified constraint (3) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(4) ((UIncreasing(69_0_REC_GE(x1[10], +(x0[10], 1))), ≥)∧[(-1)bso_40] ≥ 0)
We simplified constraint (4) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(5) ((UIncreasing(69_0_REC_GE(x1[10], +(x0[10], 1))), ≥)∧0 = 0∧[(-1)bso_40] ≥ 0)
For Pair
321_2_REC_INVOKEMETHOD(
321_1_test_InvokeMethod(
220_0_descend_Return,
x0[9]),
x1[9],
x0[9]) →
COND_321_2_REC_INVOKEMETHOD(
>(
x0[9],
0),
321_1_test_InvokeMethod(
220_0_descend_Return,
x0[9]),
x1[9],
x0[9]) the following chains were created:
- We consider the chain 321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9]) → COND_321_2_REC_INVOKEMETHOD(>(x0[9], 0), 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9]), COND_321_2_REC_INVOKEMETHOD(TRUE, 321_1_test_InvokeMethod(220_0_descend_Return, x0[10]), x1[10], x0[10]) → 69_0_REC_GE(x1[10], +(x0[10], 1)) which results in the following constraint:
(6) (>(x0[9], 0)=TRUE∧321_1_test_InvokeMethod(220_0_descend_Return, x0[9])=321_1_test_InvokeMethod(220_0_descend_Return, x0[10])∧x1[9]=x1[10]∧x0[9]=x0[10] ⇒ 321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])≥NonInfC∧321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])≥COND_321_2_REC_INVOKEMETHOD(>(x0[9], 0), 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])∧(UIncreasing(COND_321_2_REC_INVOKEMETHOD(>(x0[9], 0), 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])), ≥))
We simplified constraint (6) using rules (I), (II), (IV), (DELETE_TRIVIAL_REDUCESTO) which results in the following new constraint:
(7) (>(x0[9], 0)=TRUE ⇒ 321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])≥NonInfC∧321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])≥COND_321_2_REC_INVOKEMETHOD(>(x0[9], 0), 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])∧(UIncreasing(COND_321_2_REC_INVOKEMETHOD(>(x0[9], 0), 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])), ≥))
We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(8) (x0[9] + [-1] ≥ 0 ⇒ (UIncreasing(COND_321_2_REC_INVOKEMETHOD(>(x0[9], 0), 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])), ≥)∧[(-1)bni_41 + (-1)Bound*bni_41] + [(-1)bni_41]x0[9] ≥ 0∧[(-1)bso_42] ≥ 0)
We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(9) (x0[9] + [-1] ≥ 0 ⇒ (UIncreasing(COND_321_2_REC_INVOKEMETHOD(>(x0[9], 0), 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])), ≥)∧[(-1)bni_41 + (-1)Bound*bni_41] + [(-1)bni_41]x0[9] ≥ 0∧[(-1)bso_42] ≥ 0)
We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(10) (x0[9] + [-1] ≥ 0 ⇒ (UIncreasing(COND_321_2_REC_INVOKEMETHOD(>(x0[9], 0), 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])), ≥)∧[(-1)bni_41 + (-1)Bound*bni_41] + [(-1)bni_41]x0[9] ≥ 0∧[(-1)bso_42] ≥ 0)
We simplified constraint (10) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(11) (x0[9] ≥ 0 ⇒ (UIncreasing(COND_321_2_REC_INVOKEMETHOD(>(x0[9], 0), 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])), ≥)∧[(-2)bni_41 + (-1)Bound*bni_41] + [(-1)bni_41]x0[9] ≥ 0∧[(-1)bso_42] ≥ 0)
For Pair
309_2_REC_INVOKEMETHOD(
309_1_test_InvokeMethod(
220_0_descend_Return,
x0[8]),
x1[8],
x0[8]) →
321_2_REC_INVOKEMETHOD(
321_1_test_InvokeMethod(
92_0_descend_Load(
x0[8]),
x0[8]),
x1[8],
x0[8]) the following chains were created:
- We consider the chain 309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(220_0_descend_Return, x0[8]), x1[8], x0[8]) → 321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]), x1[8], x0[8]) which results in the following constraint:
(12) (309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(220_0_descend_Return, x0[8]), x1[8], x0[8])≥NonInfC∧309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(220_0_descend_Return, x0[8]), x1[8], x0[8])≥321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]), x1[8], x0[8])∧(UIncreasing(321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]), x1[8], x0[8])), ≥))
We simplified constraint (12) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(13) ((UIncreasing(321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]), x1[8], x0[8])), ≥)∧[(-1)bso_44] ≥ 0)
We simplified constraint (13) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(14) ((UIncreasing(321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]), x1[8], x0[8])), ≥)∧[(-1)bso_44] ≥ 0)
We simplified constraint (14) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(15) ((UIncreasing(321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]), x1[8], x0[8])), ≥)∧[(-1)bso_44] ≥ 0)
We simplified constraint (15) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(16) ((UIncreasing(321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]), x1[8], x0[8])), ≥)∧0 = 0∧[(-1)bso_44] ≥ 0)
For Pair
295_2_REC_INVOKEMETHOD(
295_1_test_InvokeMethod(
220_0_descend_Return,
x0[7]),
x1[7],
x0[7]) →
309_2_REC_INVOKEMETHOD(
309_1_test_InvokeMethod(
92_0_descend_Load(
x0[7]),
x0[7]),
x1[7],
x0[7]) the following chains were created:
- We consider the chain 295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(220_0_descend_Return, x0[7]), x1[7], x0[7]) → 309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]), x1[7], x0[7]) which results in the following constraint:
(17) (295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(220_0_descend_Return, x0[7]), x1[7], x0[7])≥NonInfC∧295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(220_0_descend_Return, x0[7]), x1[7], x0[7])≥309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]), x1[7], x0[7])∧(UIncreasing(309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]), x1[7], x0[7])), ≥))
We simplified constraint (17) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(18) ((UIncreasing(309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]), x1[7], x0[7])), ≥)∧[(-1)bso_46] ≥ 0)
We simplified constraint (18) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(19) ((UIncreasing(309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]), x1[7], x0[7])), ≥)∧[(-1)bso_46] ≥ 0)
We simplified constraint (19) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(20) ((UIncreasing(309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]), x1[7], x0[7])), ≥)∧[(-1)bso_46] ≥ 0)
We simplified constraint (20) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(21) ((UIncreasing(309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]), x1[7], x0[7])), ≥)∧0 = 0∧[(-1)bso_46] ≥ 0)
For Pair
282_2_REC_INVOKEMETHOD(
282_1_test_InvokeMethod(
220_0_descend_Return,
x0[6]),
x1[6],
x0[6]) →
295_2_REC_INVOKEMETHOD(
295_1_test_InvokeMethod(
92_0_descend_Load(
x0[6]),
x0[6]),
x1[6],
x0[6]) the following chains were created:
- We consider the chain 282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(220_0_descend_Return, x0[6]), x1[6], x0[6]) → 295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]), x1[6], x0[6]) which results in the following constraint:
(22) (282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(220_0_descend_Return, x0[6]), x1[6], x0[6])≥NonInfC∧282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(220_0_descend_Return, x0[6]), x1[6], x0[6])≥295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]), x1[6], x0[6])∧(UIncreasing(295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]), x1[6], x0[6])), ≥))
We simplified constraint (22) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(23) ((UIncreasing(295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]), x1[6], x0[6])), ≥)∧[(-1)bso_48] ≥ 0)
We simplified constraint (23) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(24) ((UIncreasing(295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]), x1[6], x0[6])), ≥)∧[(-1)bso_48] ≥ 0)
We simplified constraint (24) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(25) ((UIncreasing(295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]), x1[6], x0[6])), ≥)∧[(-1)bso_48] ≥ 0)
We simplified constraint (25) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(26) ((UIncreasing(295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]), x1[6], x0[6])), ≥)∧0 = 0∧[(-1)bso_48] ≥ 0)
For Pair
266_2_REC_INVOKEMETHOD(
266_1_test_InvokeMethod(
220_0_descend_Return,
x0[5]),
x1[5],
x0[5]) →
282_2_REC_INVOKEMETHOD(
282_1_test_InvokeMethod(
92_0_descend_Load(
x0[5]),
x0[5]),
x1[5],
x0[5]) the following chains were created:
- We consider the chain 266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(220_0_descend_Return, x0[5]), x1[5], x0[5]) → 282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]), x1[5], x0[5]) which results in the following constraint:
(27) (266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(220_0_descend_Return, x0[5]), x1[5], x0[5])≥NonInfC∧266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(220_0_descend_Return, x0[5]), x1[5], x0[5])≥282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]), x1[5], x0[5])∧(UIncreasing(282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]), x1[5], x0[5])), ≥))
We simplified constraint (27) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(28) ((UIncreasing(282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]), x1[5], x0[5])), ≥)∧[(-1)bso_50] ≥ 0)
We simplified constraint (28) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(29) ((UIncreasing(282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]), x1[5], x0[5])), ≥)∧[(-1)bso_50] ≥ 0)
We simplified constraint (29) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(30) ((UIncreasing(282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]), x1[5], x0[5])), ≥)∧[(-1)bso_50] ≥ 0)
We simplified constraint (30) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(31) ((UIncreasing(282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]), x1[5], x0[5])), ≥)∧0 = 0∧[(-1)bso_50] ≥ 0)
For Pair
250_2_REC_INVOKEMETHOD(
250_1_test_InvokeMethod(
220_0_descend_Return,
x0[4]),
x1[4],
x0[4]) →
266_2_REC_INVOKEMETHOD(
266_1_test_InvokeMethod(
92_0_descend_Load(
x0[4]),
x0[4]),
x1[4],
x0[4]) the following chains were created:
- We consider the chain 250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(220_0_descend_Return, x0[4]), x1[4], x0[4]) → 266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]), x1[4], x0[4]) which results in the following constraint:
(32) (250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(220_0_descend_Return, x0[4]), x1[4], x0[4])≥NonInfC∧250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(220_0_descend_Return, x0[4]), x1[4], x0[4])≥266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]), x1[4], x0[4])∧(UIncreasing(266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]), x1[4], x0[4])), ≥))
We simplified constraint (32) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(33) ((UIncreasing(266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]), x1[4], x0[4])), ≥)∧[(-1)bso_52] ≥ 0)
We simplified constraint (33) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(34) ((UIncreasing(266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]), x1[4], x0[4])), ≥)∧[(-1)bso_52] ≥ 0)
We simplified constraint (34) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(35) ((UIncreasing(266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]), x1[4], x0[4])), ≥)∧[(-1)bso_52] ≥ 0)
We simplified constraint (35) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(36) ((UIncreasing(266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]), x1[4], x0[4])), ≥)∧0 = 0∧[(-1)bso_52] ≥ 0)
For Pair
237_2_REC_INVOKEMETHOD(
237_1_test_InvokeMethod(
220_0_descend_Return,
x0[3]),
x1[3],
x0[3]) →
250_2_REC_INVOKEMETHOD(
250_1_test_InvokeMethod(
92_0_descend_Load(
x0[3]),
x0[3]),
x1[3],
x0[3]) the following chains were created:
- We consider the chain 237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(220_0_descend_Return, x0[3]), x1[3], x0[3]) → 250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]), x1[3], x0[3]) which results in the following constraint:
(37) (237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(220_0_descend_Return, x0[3]), x1[3], x0[3])≥NonInfC∧237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(220_0_descend_Return, x0[3]), x1[3], x0[3])≥250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]), x1[3], x0[3])∧(UIncreasing(250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]), x1[3], x0[3])), ≥))
We simplified constraint (37) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(38) ((UIncreasing(250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]), x1[3], x0[3])), ≥)∧[(-1)bso_54] ≥ 0)
We simplified constraint (38) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(39) ((UIncreasing(250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]), x1[3], x0[3])), ≥)∧[(-1)bso_54] ≥ 0)
We simplified constraint (39) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(40) ((UIncreasing(250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]), x1[3], x0[3])), ≥)∧[(-1)bso_54] ≥ 0)
We simplified constraint (40) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(41) ((UIncreasing(250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]), x1[3], x0[3])), ≥)∧0 = 0∧[(-1)bso_54] ≥ 0)
For Pair
92_2_REC_INVOKEMETHOD(
92_1_test_InvokeMethod(
220_0_descend_Return,
x0[2]),
x1[2],
x0[2]) →
237_2_REC_INVOKEMETHOD(
237_1_test_InvokeMethod(
92_0_descend_Load(
x0[2]),
x0[2]),
x1[2],
x0[2]) the following chains were created:
- We consider the chain 92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(220_0_descend_Return, x0[2]), x1[2], x0[2]) → 237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(92_0_descend_Load(x0[2]), x0[2]), x1[2], x0[2]) which results in the following constraint:
(42) (92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(220_0_descend_Return, x0[2]), x1[2], x0[2])≥NonInfC∧92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(220_0_descend_Return, x0[2]), x1[2], x0[2])≥237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(92_0_descend_Load(x0[2]), x0[2]), x1[2], x0[2])∧(UIncreasing(237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(92_0_descend_Load(x0[2]), x0[2]), x1[2], x0[2])), ≥))
We simplified constraint (42) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(43) ((UIncreasing(237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(92_0_descend_Load(x0[2]), x0[2]), x1[2], x0[2])), ≥)∧[(-1)bso_56] ≥ 0)
We simplified constraint (43) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(44) ((UIncreasing(237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(92_0_descend_Load(x0[2]), x0[2]), x1[2], x0[2])), ≥)∧[(-1)bso_56] ≥ 0)
We simplified constraint (44) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(45) ((UIncreasing(237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(92_0_descend_Load(x0[2]), x0[2]), x1[2], x0[2])), ≥)∧[(-1)bso_56] ≥ 0)
We simplified constraint (45) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(46) ((UIncreasing(237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(92_0_descend_Load(x0[2]), x0[2]), x1[2], x0[2])), ≥)∧0 = 0∧[(-1)bso_56] ≥ 0)
For Pair
COND_69_0_REC_GE(
TRUE,
x0[1],
x1[1]) →
92_2_REC_INVOKEMETHOD(
92_1_test_InvokeMethod(
92_0_descend_Load(
x1[1]),
x1[1]),
x0[1],
x1[1]) the following chains were created:
- We consider the chain COND_69_0_REC_GE(TRUE, x0[1], x1[1]) → 92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]), x0[1], x1[1]) which results in the following constraint:
(47) (COND_69_0_REC_GE(TRUE, x0[1], x1[1])≥NonInfC∧COND_69_0_REC_GE(TRUE, x0[1], x1[1])≥92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]), x0[1], x1[1])∧(UIncreasing(92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]), x0[1], x1[1])), ≥))
We simplified constraint (47) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(48) ((UIncreasing(92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]), x0[1], x1[1])), ≥)∧[(-1)bso_58] ≥ 0)
We simplified constraint (48) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(49) ((UIncreasing(92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]), x0[1], x1[1])), ≥)∧[(-1)bso_58] ≥ 0)
We simplified constraint (49) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(50) ((UIncreasing(92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]), x0[1], x1[1])), ≥)∧[(-1)bso_58] ≥ 0)
We simplified constraint (50) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(51) ((UIncreasing(92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]), x0[1], x1[1])), ≥)∧0 = 0∧[(-1)bso_58] ≥ 0)
For Pair
69_0_REC_GE(
x0[0],
x1[0]) →
COND_69_0_REC_GE(
<(
x1[0],
100),
x0[0],
x1[0]) the following chains were created:
- We consider the chain 69_0_REC_GE(x0[0], x1[0]) → COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0]), COND_69_0_REC_GE(TRUE, x0[1], x1[1]) → 92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]), x0[1], x1[1]) which results in the following constraint:
(52) (<(x1[0], 100)=TRUE∧x0[0]=x0[1]∧x1[0]=x1[1] ⇒ 69_0_REC_GE(x0[0], x1[0])≥NonInfC∧69_0_REC_GE(x0[0], x1[0])≥COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])∧(UIncreasing(COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥))
We simplified constraint (52) using rule (IV) which results in the following new constraint:
(53) (<(x1[0], 100)=TRUE ⇒ 69_0_REC_GE(x0[0], x1[0])≥NonInfC∧69_0_REC_GE(x0[0], x1[0])≥COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])∧(UIncreasing(COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥))
We simplified constraint (53) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(54) ([99] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)Bound*bni_59] + [(-1)bni_59]x1[0] ≥ 0∧[1 + (-1)bso_60] ≥ 0)
We simplified constraint (54) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(55) ([99] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)Bound*bni_59] + [(-1)bni_59]x1[0] ≥ 0∧[1 + (-1)bso_60] ≥ 0)
We simplified constraint (55) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(56) ([99] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)Bound*bni_59] + [(-1)bni_59]x1[0] ≥ 0∧[1 + (-1)bso_60] ≥ 0)
We simplified constraint (56) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
(57) ([99] + [-1]x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)Bound*bni_59] + [(-1)bni_59]x1[0] ≥ 0∧[1 + (-1)bso_60] ≥ 0)
(58) ([99] + x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)Bound*bni_59] + [bni_59]x1[0] ≥ 0∧[1 + (-1)bso_60] ≥ 0)
To summarize, we get the following constraints P
≥ for the following pairs.
- COND_321_2_REC_INVOKEMETHOD(TRUE, 321_1_test_InvokeMethod(220_0_descend_Return, x0[10]), x1[10], x0[10]) → 69_0_REC_GE(x1[10], +(x0[10], 1))
- ((UIncreasing(69_0_REC_GE(x1[10], +(x0[10], 1))), ≥)∧0 = 0∧[(-1)bso_40] ≥ 0)
- 321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9]) → COND_321_2_REC_INVOKEMETHOD(>(x0[9], 0), 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])
- (x0[9] ≥ 0 ⇒ (UIncreasing(COND_321_2_REC_INVOKEMETHOD(>(x0[9], 0), 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])), ≥)∧[(-2)bni_41 + (-1)Bound*bni_41] + [(-1)bni_41]x0[9] ≥ 0∧[(-1)bso_42] ≥ 0)
- 309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(220_0_descend_Return, x0[8]), x1[8], x0[8]) → 321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]), x1[8], x0[8])
- ((UIncreasing(321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]), x1[8], x0[8])), ≥)∧0 = 0∧[(-1)bso_44] ≥ 0)
- 295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(220_0_descend_Return, x0[7]), x1[7], x0[7]) → 309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]), x1[7], x0[7])
- ((UIncreasing(309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]), x1[7], x0[7])), ≥)∧0 = 0∧[(-1)bso_46] ≥ 0)
- 282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(220_0_descend_Return, x0[6]), x1[6], x0[6]) → 295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]), x1[6], x0[6])
- ((UIncreasing(295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]), x1[6], x0[6])), ≥)∧0 = 0∧[(-1)bso_48] ≥ 0)
- 266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(220_0_descend_Return, x0[5]), x1[5], x0[5]) → 282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]), x1[5], x0[5])
- ((UIncreasing(282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]), x1[5], x0[5])), ≥)∧0 = 0∧[(-1)bso_50] ≥ 0)
- 250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(220_0_descend_Return, x0[4]), x1[4], x0[4]) → 266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]), x1[4], x0[4])
- ((UIncreasing(266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]), x1[4], x0[4])), ≥)∧0 = 0∧[(-1)bso_52] ≥ 0)
- 237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(220_0_descend_Return, x0[3]), x1[3], x0[3]) → 250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]), x1[3], x0[3])
- ((UIncreasing(250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]), x1[3], x0[3])), ≥)∧0 = 0∧[(-1)bso_54] ≥ 0)
- 92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(220_0_descend_Return, x0[2]), x1[2], x0[2]) → 237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(92_0_descend_Load(x0[2]), x0[2]), x1[2], x0[2])
- ((UIncreasing(237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(92_0_descend_Load(x0[2]), x0[2]), x1[2], x0[2])), ≥)∧0 = 0∧[(-1)bso_56] ≥ 0)
- COND_69_0_REC_GE(TRUE, x0[1], x1[1]) → 92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]), x0[1], x1[1])
- ((UIncreasing(92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]), x0[1], x1[1])), ≥)∧0 = 0∧[(-1)bso_58] ≥ 0)
- 69_0_REC_GE(x0[0], x1[0]) → COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])
- ([99] + [-1]x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)Bound*bni_59] + [(-1)bni_59]x1[0] ≥ 0∧[1 + (-1)bso_60] ≥ 0)
- ([99] + x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)Bound*bni_59] + [bni_59]x1[0] ≥ 0∧[1 + (-1)bso_60] ≥ 0)
The constraints for P
> respective P
bound are constructed from P
≥ where we just replace every occurence of "t ≥ s" in P
≥ by "t > s" respective "t ≥
c". Here
c stands for the fresh constant used for P
bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:
POL(TRUE) = 0
POL(FALSE) = 0
POL(92_0_descend_Load(x1)) = [-1] + [-1]x1
POL(181_0_descend_Return) = [-1]
POL(243_0_descend_Return) = [-1]
POL(256_0_descend_Return) = [-1]
POL(273_0_descend_Return) = [1]
POL(287_0_descend_Return) = 0
POL(300_0_descend_Return) = 0
POL(314_0_descend_Return) = [1]
POL(327_0_descend_Return) = [2]
POL(169_0_descend_LE(x1)) = [2]
POL(0) = 0
POL(175_0_descend_Return) = [1]
POL(Cond_169_0_descend_LE(x1, x2)) = [-1]x2
POL(>(x1, x2)) = [-1]
POL(191_1_descend_InvokeMethod(x1, x2)) = [-1] + [-1]x2 + [-1]x1
POL(-(x1, x2)) = x1 + [-1]x2
POL(1) = [1]
POL(220_0_descend_Return) = [-1]
POL(COND_321_2_REC_INVOKEMETHOD(x1, x2, x3, x4)) = [-1] + [-1]x4
POL(321_1_test_InvokeMethod(x1, x2)) = [-1] + [-1]x2 + [-1]x1
POL(69_0_REC_GE(x1, x2)) = [-1]x2
POL(+(x1, x2)) = x1 + x2
POL(321_2_REC_INVOKEMETHOD(x1, x2, x3)) = [-1] + [-1]x3
POL(309_2_REC_INVOKEMETHOD(x1, x2, x3)) = [-1] + [-1]x3
POL(309_1_test_InvokeMethod(x1, x2)) = [-1] + [-1]x2 + [-1]x1
POL(295_2_REC_INVOKEMETHOD(x1, x2, x3)) = [-1] + [-1]x3
POL(295_1_test_InvokeMethod(x1, x2)) = [-1] + [-1]x1
POL(282_2_REC_INVOKEMETHOD(x1, x2, x3)) = [-1] + [-1]x3
POL(282_1_test_InvokeMethod(x1, x2)) = [-1] + [-1]x2 + [-1]x1
POL(266_2_REC_INVOKEMETHOD(x1, x2, x3)) = [-1] + [-1]x3
POL(266_1_test_InvokeMethod(x1, x2)) = [-1] + [2]x2 + [-1]x1
POL(250_2_REC_INVOKEMETHOD(x1, x2, x3)) = [-1] + [-1]x3
POL(250_1_test_InvokeMethod(x1, x2)) = [-1] + [-1]x2 + [-1]x1
POL(237_2_REC_INVOKEMETHOD(x1, x2, x3)) = [-1] + [-1]x1 + [-1]x3
POL(237_1_test_InvokeMethod(x1, x2)) = 0
POL(92_2_REC_INVOKEMETHOD(x1, x2, x3)) = [-1]x1 + [-1]x3
POL(92_1_test_InvokeMethod(x1, x2)) = [1]
POL(COND_69_0_REC_GE(x1, x2, x3)) = [-1] + [-1]x3
POL(<(x1, x2)) = [-1]
POL(100) = [100]
The following pairs are in P
>:
69_0_REC_GE(x0[0], x1[0]) → COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])
The following pairs are in P
bound:
69_0_REC_GE(x0[0], x1[0]) → COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])
The following pairs are in P
≥:
COND_321_2_REC_INVOKEMETHOD(TRUE, 321_1_test_InvokeMethod(220_0_descend_Return, x0[10]), x1[10], x0[10]) → 69_0_REC_GE(x1[10], +(x0[10], 1))
321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9]) → COND_321_2_REC_INVOKEMETHOD(>(x0[9], 0), 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])
309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(220_0_descend_Return, x0[8]), x1[8], x0[8]) → 321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]), x1[8], x0[8])
295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(220_0_descend_Return, x0[7]), x1[7], x0[7]) → 309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]), x1[7], x0[7])
282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(220_0_descend_Return, x0[6]), x1[6], x0[6]) → 295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]), x1[6], x0[6])
266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(220_0_descend_Return, x0[5]), x1[5], x0[5]) → 282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]), x1[5], x0[5])
250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(220_0_descend_Return, x0[4]), x1[4], x0[4]) → 266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]), x1[4], x0[4])
237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(220_0_descend_Return, x0[3]), x1[3], x0[3]) → 250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]), x1[3], x0[3])
92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(220_0_descend_Return, x0[2]), x1[2], x0[2]) → 237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(92_0_descend_Load(x0[2]), x0[2]), x1[2], x0[2])
COND_69_0_REC_GE(TRUE, x0[1], x1[1]) → 92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]), x0[1], x1[1])
At least the following rules have been oriented under context sensitive arithmetic replacement:
169_0_descend_LE(0)1 → 175_0_descend_Return1
220_0_descend_Return1 → 191_1_descend_InvokeMethod(175_0_descend_Return, 0)1
(23) Obligation:
IDP problem:
The following function symbols are pre-defined:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
| ~ | Bwxor: (Integer, Integer) -> Integer |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
The following domains are used:
Integer
The ITRS R consists of the following rules:
92_0_descend_Load(
i12) →
181_0_descend_Return92_0_descend_Load(
i45) →
243_0_descend_Return92_0_descend_Load(
i59) →
256_0_descend_Return92_0_descend_Load(
i62) →
273_0_descend_Return92_0_descend_Load(
i67) →
287_0_descend_Return92_0_descend_Load(
i70) →
300_0_descend_Return92_0_descend_Load(
i74) →
314_0_descend_Return92_0_descend_Load(
i76) →
327_0_descend_Return92_0_descend_Load(
x0) →
169_0_descend_LE(
x0)
169_0_descend_LE(
0) →
175_0_descend_Return169_0_descend_LE(
x0) →
Cond_169_0_descend_LE(
x0 > 0,
x0)
Cond_169_0_descend_LE(
TRUE,
x0) →
191_1_descend_InvokeMethod(
169_0_descend_LE(
x0 - 1),
x0 - 1)
191_1_descend_InvokeMethod(
175_0_descend_Return,
0) →
220_0_descend_Return191_1_descend_InvokeMethod(
220_0_descend_Return,
x0) →
220_0_descend_ReturnThe integer pair graph contains the following rules and edges:
(10):
COND_321_2_REC_INVOKEMETHOD(
TRUE,
321_1_test_InvokeMethod(
220_0_descend_Return,
x0[10]),
x1[10],
x0[10]) →
69_0_REC_GE(
x1[10],
x0[10] + 1)
(9):
321_2_REC_INVOKEMETHOD(
321_1_test_InvokeMethod(
220_0_descend_Return,
x0[9]),
x1[9],
x0[9]) →
COND_321_2_REC_INVOKEMETHOD(
x0[9] > 0,
321_1_test_InvokeMethod(
220_0_descend_Return,
x0[9]),
x1[9],
x0[9])
(8):
309_2_REC_INVOKEMETHOD(
309_1_test_InvokeMethod(
220_0_descend_Return,
x0[8]),
x1[8],
x0[8]) →
321_2_REC_INVOKEMETHOD(
321_1_test_InvokeMethod(
92_0_descend_Load(
x0[8]),
x0[8]),
x1[8],
x0[8])
(7):
295_2_REC_INVOKEMETHOD(
295_1_test_InvokeMethod(
220_0_descend_Return,
x0[7]),
x1[7],
x0[7]) →
309_2_REC_INVOKEMETHOD(
309_1_test_InvokeMethod(
92_0_descend_Load(
x0[7]),
x0[7]),
x1[7],
x0[7])
(6):
282_2_REC_INVOKEMETHOD(
282_1_test_InvokeMethod(
220_0_descend_Return,
x0[6]),
x1[6],
x0[6]) →
295_2_REC_INVOKEMETHOD(
295_1_test_InvokeMethod(
92_0_descend_Load(
x0[6]),
x0[6]),
x1[6],
x0[6])
(5):
266_2_REC_INVOKEMETHOD(
266_1_test_InvokeMethod(
220_0_descend_Return,
x0[5]),
x1[5],
x0[5]) →
282_2_REC_INVOKEMETHOD(
282_1_test_InvokeMethod(
92_0_descend_Load(
x0[5]),
x0[5]),
x1[5],
x0[5])
(4):
250_2_REC_INVOKEMETHOD(
250_1_test_InvokeMethod(
220_0_descend_Return,
x0[4]),
x1[4],
x0[4]) →
266_2_REC_INVOKEMETHOD(
266_1_test_InvokeMethod(
92_0_descend_Load(
x0[4]),
x0[4]),
x1[4],
x0[4])
(3):
237_2_REC_INVOKEMETHOD(
237_1_test_InvokeMethod(
220_0_descend_Return,
x0[3]),
x1[3],
x0[3]) →
250_2_REC_INVOKEMETHOD(
250_1_test_InvokeMethod(
92_0_descend_Load(
x0[3]),
x0[3]),
x1[3],
x0[3])
(2):
92_2_REC_INVOKEMETHOD(
92_1_test_InvokeMethod(
220_0_descend_Return,
x0[2]),
x1[2],
x0[2]) →
237_2_REC_INVOKEMETHOD(
237_1_test_InvokeMethod(
92_0_descend_Load(
x0[2]),
x0[2]),
x1[2],
x0[2])
(1):
COND_69_0_REC_GE(
TRUE,
x0[1],
x1[1]) →
92_2_REC_INVOKEMETHOD(
92_1_test_InvokeMethod(
92_0_descend_Load(
x1[1]),
x1[1]),
x0[1],
x1[1])
(1) -> (2), if ((92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]) →* 92_1_test_InvokeMethod(220_0_descend_Return, x0[2]))∧(x0[1] →* x1[2])∧(x1[1] →* x0[2]))
(2) -> (3), if ((237_1_test_InvokeMethod(92_0_descend_Load(x0[2]), x0[2]) →* 237_1_test_InvokeMethod(220_0_descend_Return, x0[3]))∧(x1[2] →* x1[3])∧(x0[2] →* x0[3]))
(3) -> (4), if ((250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]) →* 250_1_test_InvokeMethod(220_0_descend_Return, x0[4]))∧(x1[3] →* x1[4])∧(x0[3] →* x0[4]))
(4) -> (5), if ((266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]) →* 266_1_test_InvokeMethod(220_0_descend_Return, x0[5]))∧(x1[4] →* x1[5])∧(x0[4] →* x0[5]))
(5) -> (6), if ((282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]) →* 282_1_test_InvokeMethod(220_0_descend_Return, x0[6]))∧(x1[5] →* x1[6])∧(x0[5] →* x0[6]))
(6) -> (7), if ((295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]) →* 295_1_test_InvokeMethod(220_0_descend_Return, x0[7]))∧(x1[6] →* x1[7])∧(x0[6] →* x0[7]))
(7) -> (8), if ((309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]) →* 309_1_test_InvokeMethod(220_0_descend_Return, x0[8]))∧(x1[7] →* x1[8])∧(x0[7] →* x0[8]))
(8) -> (9), if ((321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]) →* 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]))∧(x1[8] →* x1[9])∧(x0[8] →* x0[9]))
(9) -> (10), if ((x0[9] > 0 →* TRUE)∧(321_1_test_InvokeMethod(220_0_descend_Return, x0[9]) →* 321_1_test_InvokeMethod(220_0_descend_Return, x0[10]))∧(x1[9] →* x1[10])∧(x0[9] →* x0[10]))
The set Q consists of the following terms:
92_0_descend_Load(
x0)
97_1_rec_InvokeMethod(
47_0_rec_Return,
0)
97_1_rec_InvokeMethod(
143_0_rec_Return,
x0)
169_0_descend_LE(
x0)
Cond_169_0_descend_LE(
TRUE,
x0)
191_1_descend_InvokeMethod(
175_0_descend_Return,
0)
191_1_descend_InvokeMethod(
220_0_descend_Return,
x0)
(24) IDependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 10 less nodes.
(25) TRUE
(26) Obligation:
IDP problem:
The following function symbols are pre-defined:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
| ~ | Bwxor: (Integer, Integer) -> Integer |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
The following domains are used:
Integer
The ITRS R consists of the following rules:
92_0_descend_Load(
i12) →
181_0_descend_Return92_0_descend_Load(
i45) →
243_0_descend_Return92_0_descend_Load(
i59) →
256_0_descend_Return92_0_descend_Load(
i62) →
273_0_descend_Return92_0_descend_Load(
i67) →
287_0_descend_Return92_0_descend_Load(
i70) →
300_0_descend_Return92_0_descend_Load(
i74) →
314_0_descend_Return92_0_descend_Load(
i76) →
327_0_descend_Return92_0_descend_Load(
x0) →
169_0_descend_LE(
x0)
97_1_rec_InvokeMethod(
47_0_rec_Return,
0) →
143_0_rec_Return97_1_rec_InvokeMethod(
143_0_rec_Return,
x0) →
143_0_rec_Return169_0_descend_LE(
0) →
175_0_descend_Return169_0_descend_LE(
x0) →
Cond_169_0_descend_LE(
x0 > 0,
x0)
Cond_169_0_descend_LE(
TRUE,
x0) →
191_1_descend_InvokeMethod(
169_0_descend_LE(
x0 - 1),
x0 - 1)
191_1_descend_InvokeMethod(
175_0_descend_Return,
0) →
220_0_descend_Return191_1_descend_InvokeMethod(
220_0_descend_Return,
x0) →
220_0_descend_ReturnThe integer pair graph contains the following rules and edges:
(0):
69_0_REC_GE(
x0[0],
x1[0]) →
COND_69_0_REC_GE(
x1[0] < 100,
x0[0],
x1[0])
(1):
COND_69_0_REC_GE(
TRUE,
x0[1],
x1[1]) →
92_2_REC_INVOKEMETHOD(
92_1_test_InvokeMethod(
92_0_descend_Load(
x1[1]),
x1[1]),
x0[1],
x1[1])
(2):
92_2_REC_INVOKEMETHOD(
92_1_test_InvokeMethod(
220_0_descend_Return,
x0[2]),
x1[2],
x0[2]) →
237_2_REC_INVOKEMETHOD(
237_1_test_InvokeMethod(
92_0_descend_Load(
x0[2]),
x0[2]),
x1[2],
x0[2])
(3):
237_2_REC_INVOKEMETHOD(
237_1_test_InvokeMethod(
220_0_descend_Return,
x0[3]),
x1[3],
x0[3]) →
250_2_REC_INVOKEMETHOD(
250_1_test_InvokeMethod(
92_0_descend_Load(
x0[3]),
x0[3]),
x1[3],
x0[3])
(4):
250_2_REC_INVOKEMETHOD(
250_1_test_InvokeMethod(
220_0_descend_Return,
x0[4]),
x1[4],
x0[4]) →
266_2_REC_INVOKEMETHOD(
266_1_test_InvokeMethod(
92_0_descend_Load(
x0[4]),
x0[4]),
x1[4],
x0[4])
(5):
266_2_REC_INVOKEMETHOD(
266_1_test_InvokeMethod(
220_0_descend_Return,
x0[5]),
x1[5],
x0[5]) →
282_2_REC_INVOKEMETHOD(
282_1_test_InvokeMethod(
92_0_descend_Load(
x0[5]),
x0[5]),
x1[5],
x0[5])
(6):
282_2_REC_INVOKEMETHOD(
282_1_test_InvokeMethod(
220_0_descend_Return,
x0[6]),
x1[6],
x0[6]) →
295_2_REC_INVOKEMETHOD(
295_1_test_InvokeMethod(
92_0_descend_Load(
x0[6]),
x0[6]),
x1[6],
x0[6])
(7):
295_2_REC_INVOKEMETHOD(
295_1_test_InvokeMethod(
220_0_descend_Return,
x0[7]),
x1[7],
x0[7]) →
309_2_REC_INVOKEMETHOD(
309_1_test_InvokeMethod(
92_0_descend_Load(
x0[7]),
x0[7]),
x1[7],
x0[7])
(8):
309_2_REC_INVOKEMETHOD(
309_1_test_InvokeMethod(
220_0_descend_Return,
x0[8]),
x1[8],
x0[8]) →
321_2_REC_INVOKEMETHOD(
321_1_test_InvokeMethod(
92_0_descend_Load(
x0[8]),
x0[8]),
x1[8],
x0[8])
(9):
321_2_REC_INVOKEMETHOD(
321_1_test_InvokeMethod(
220_0_descend_Return,
x0[9]),
x1[9],
x0[9]) →
COND_321_2_REC_INVOKEMETHOD(
x0[9] > 0,
321_1_test_InvokeMethod(
220_0_descend_Return,
x0[9]),
x1[9],
x0[9])
(10):
COND_321_2_REC_INVOKEMETHOD(
TRUE,
321_1_test_InvokeMethod(
220_0_descend_Return,
x0[10]),
x1[10],
x0[10]) →
69_0_REC_GE(
x1[10],
x0[10] + 1)
(12):
COND_69_0_REC_GE1(
TRUE,
x0[12],
x1[12]) →
69_0_REC_GE(
x0[12] - 1,
x0[12] - 1)
(10) -> (0), if ((x1[10] →* x0[0])∧(x0[10] + 1 →* x1[0]))
(12) -> (0), if ((x0[12] - 1 →* x0[0])∧(x0[12] - 1 →* x1[0]))
(0) -> (1), if ((x1[0] < 100 →* TRUE)∧(x0[0] →* x0[1])∧(x1[0] →* x1[1]))
(1) -> (2), if ((92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]) →* 92_1_test_InvokeMethod(220_0_descend_Return, x0[2]))∧(x0[1] →* x1[2])∧(x1[1] →* x0[2]))
(2) -> (3), if ((237_1_test_InvokeMethod(92_0_descend_Load(x0[2]), x0[2]) →* 237_1_test_InvokeMethod(220_0_descend_Return, x0[3]))∧(x1[2] →* x1[3])∧(x0[2] →* x0[3]))
(3) -> (4), if ((250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]) →* 250_1_test_InvokeMethod(220_0_descend_Return, x0[4]))∧(x1[3] →* x1[4])∧(x0[3] →* x0[4]))
(4) -> (5), if ((266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]) →* 266_1_test_InvokeMethod(220_0_descend_Return, x0[5]))∧(x1[4] →* x1[5])∧(x0[4] →* x0[5]))
(5) -> (6), if ((282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]) →* 282_1_test_InvokeMethod(220_0_descend_Return, x0[6]))∧(x1[5] →* x1[6])∧(x0[5] →* x0[6]))
(6) -> (7), if ((295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]) →* 295_1_test_InvokeMethod(220_0_descend_Return, x0[7]))∧(x1[6] →* x1[7])∧(x0[6] →* x0[7]))
(7) -> (8), if ((309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]) →* 309_1_test_InvokeMethod(220_0_descend_Return, x0[8]))∧(x1[7] →* x1[8])∧(x0[7] →* x0[8]))
(8) -> (9), if ((321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]) →* 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]))∧(x1[8] →* x1[9])∧(x0[8] →* x0[9]))
(9) -> (10), if ((x0[9] > 0 →* TRUE)∧(321_1_test_InvokeMethod(220_0_descend_Return, x0[9]) →* 321_1_test_InvokeMethod(220_0_descend_Return, x0[10]))∧(x1[9] →* x1[10])∧(x0[9] →* x0[10]))
The set Q consists of the following terms:
92_0_descend_Load(
x0)
97_1_rec_InvokeMethod(
47_0_rec_Return,
0)
97_1_rec_InvokeMethod(
143_0_rec_Return,
x0)
169_0_descend_LE(
x0)
Cond_169_0_descend_LE(
TRUE,
x0)
191_1_descend_InvokeMethod(
175_0_descend_Return,
0)
191_1_descend_InvokeMethod(
220_0_descend_Return,
x0)
(27) IDependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(28) Obligation:
IDP problem:
The following function symbols are pre-defined:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
| ~ | Bwxor: (Integer, Integer) -> Integer |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
The following domains are used:
Integer
The ITRS R consists of the following rules:
92_0_descend_Load(
i12) →
181_0_descend_Return92_0_descend_Load(
i45) →
243_0_descend_Return92_0_descend_Load(
i59) →
256_0_descend_Return92_0_descend_Load(
i62) →
273_0_descend_Return92_0_descend_Load(
i67) →
287_0_descend_Return92_0_descend_Load(
i70) →
300_0_descend_Return92_0_descend_Load(
i74) →
314_0_descend_Return92_0_descend_Load(
i76) →
327_0_descend_Return92_0_descend_Load(
x0) →
169_0_descend_LE(
x0)
97_1_rec_InvokeMethod(
47_0_rec_Return,
0) →
143_0_rec_Return97_1_rec_InvokeMethod(
143_0_rec_Return,
x0) →
143_0_rec_Return169_0_descend_LE(
0) →
175_0_descend_Return169_0_descend_LE(
x0) →
Cond_169_0_descend_LE(
x0 > 0,
x0)
Cond_169_0_descend_LE(
TRUE,
x0) →
191_1_descend_InvokeMethod(
169_0_descend_LE(
x0 - 1),
x0 - 1)
191_1_descend_InvokeMethod(
175_0_descend_Return,
0) →
220_0_descend_Return191_1_descend_InvokeMethod(
220_0_descend_Return,
x0) →
220_0_descend_ReturnThe integer pair graph contains the following rules and edges:
(10):
COND_321_2_REC_INVOKEMETHOD(
TRUE,
321_1_test_InvokeMethod(
220_0_descend_Return,
x0[10]),
x1[10],
x0[10]) →
69_0_REC_GE(
x1[10],
x0[10] + 1)
(9):
321_2_REC_INVOKEMETHOD(
321_1_test_InvokeMethod(
220_0_descend_Return,
x0[9]),
x1[9],
x0[9]) →
COND_321_2_REC_INVOKEMETHOD(
x0[9] > 0,
321_1_test_InvokeMethod(
220_0_descend_Return,
x0[9]),
x1[9],
x0[9])
(8):
309_2_REC_INVOKEMETHOD(
309_1_test_InvokeMethod(
220_0_descend_Return,
x0[8]),
x1[8],
x0[8]) →
321_2_REC_INVOKEMETHOD(
321_1_test_InvokeMethod(
92_0_descend_Load(
x0[8]),
x0[8]),
x1[8],
x0[8])
(7):
295_2_REC_INVOKEMETHOD(
295_1_test_InvokeMethod(
220_0_descend_Return,
x0[7]),
x1[7],
x0[7]) →
309_2_REC_INVOKEMETHOD(
309_1_test_InvokeMethod(
92_0_descend_Load(
x0[7]),
x0[7]),
x1[7],
x0[7])
(6):
282_2_REC_INVOKEMETHOD(
282_1_test_InvokeMethod(
220_0_descend_Return,
x0[6]),
x1[6],
x0[6]) →
295_2_REC_INVOKEMETHOD(
295_1_test_InvokeMethod(
92_0_descend_Load(
x0[6]),
x0[6]),
x1[6],
x0[6])
(5):
266_2_REC_INVOKEMETHOD(
266_1_test_InvokeMethod(
220_0_descend_Return,
x0[5]),
x1[5],
x0[5]) →
282_2_REC_INVOKEMETHOD(
282_1_test_InvokeMethod(
92_0_descend_Load(
x0[5]),
x0[5]),
x1[5],
x0[5])
(4):
250_2_REC_INVOKEMETHOD(
250_1_test_InvokeMethod(
220_0_descend_Return,
x0[4]),
x1[4],
x0[4]) →
266_2_REC_INVOKEMETHOD(
266_1_test_InvokeMethod(
92_0_descend_Load(
x0[4]),
x0[4]),
x1[4],
x0[4])
(3):
237_2_REC_INVOKEMETHOD(
237_1_test_InvokeMethod(
220_0_descend_Return,
x0[3]),
x1[3],
x0[3]) →
250_2_REC_INVOKEMETHOD(
250_1_test_InvokeMethod(
92_0_descend_Load(
x0[3]),
x0[3]),
x1[3],
x0[3])
(2):
92_2_REC_INVOKEMETHOD(
92_1_test_InvokeMethod(
220_0_descend_Return,
x0[2]),
x1[2],
x0[2]) →
237_2_REC_INVOKEMETHOD(
237_1_test_InvokeMethod(
92_0_descend_Load(
x0[2]),
x0[2]),
x1[2],
x0[2])
(1):
COND_69_0_REC_GE(
TRUE,
x0[1],
x1[1]) →
92_2_REC_INVOKEMETHOD(
92_1_test_InvokeMethod(
92_0_descend_Load(
x1[1]),
x1[1]),
x0[1],
x1[1])
(0):
69_0_REC_GE(
x0[0],
x1[0]) →
COND_69_0_REC_GE(
x1[0] < 100,
x0[0],
x1[0])
(10) -> (0), if ((x1[10] →* x0[0])∧(x0[10] + 1 →* x1[0]))
(0) -> (1), if ((x1[0] < 100 →* TRUE)∧(x0[0] →* x0[1])∧(x1[0] →* x1[1]))
(1) -> (2), if ((92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]) →* 92_1_test_InvokeMethod(220_0_descend_Return, x0[2]))∧(x0[1] →* x1[2])∧(x1[1] →* x0[2]))
(2) -> (3), if ((237_1_test_InvokeMethod(92_0_descend_Load(x0[2]), x0[2]) →* 237_1_test_InvokeMethod(220_0_descend_Return, x0[3]))∧(x1[2] →* x1[3])∧(x0[2] →* x0[3]))
(3) -> (4), if ((250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]) →* 250_1_test_InvokeMethod(220_0_descend_Return, x0[4]))∧(x1[3] →* x1[4])∧(x0[3] →* x0[4]))
(4) -> (5), if ((266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]) →* 266_1_test_InvokeMethod(220_0_descend_Return, x0[5]))∧(x1[4] →* x1[5])∧(x0[4] →* x0[5]))
(5) -> (6), if ((282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]) →* 282_1_test_InvokeMethod(220_0_descend_Return, x0[6]))∧(x1[5] →* x1[6])∧(x0[5] →* x0[6]))
(6) -> (7), if ((295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]) →* 295_1_test_InvokeMethod(220_0_descend_Return, x0[7]))∧(x1[6] →* x1[7])∧(x0[6] →* x0[7]))
(7) -> (8), if ((309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]) →* 309_1_test_InvokeMethod(220_0_descend_Return, x0[8]))∧(x1[7] →* x1[8])∧(x0[7] →* x0[8]))
(8) -> (9), if ((321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]) →* 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]))∧(x1[8] →* x1[9])∧(x0[8] →* x0[9]))
(9) -> (10), if ((x0[9] > 0 →* TRUE)∧(321_1_test_InvokeMethod(220_0_descend_Return, x0[9]) →* 321_1_test_InvokeMethod(220_0_descend_Return, x0[10]))∧(x1[9] →* x1[10])∧(x0[9] →* x0[10]))
The set Q consists of the following terms:
92_0_descend_Load(
x0)
97_1_rec_InvokeMethod(
47_0_rec_Return,
0)
97_1_rec_InvokeMethod(
143_0_rec_Return,
x0)
169_0_descend_LE(
x0)
Cond_169_0_descend_LE(
TRUE,
x0)
191_1_descend_InvokeMethod(
175_0_descend_Return,
0)
191_1_descend_InvokeMethod(
220_0_descend_Return,
x0)
(29) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(30) Obligation:
IDP problem:
The following function symbols are pre-defined:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
| ~ | Bwxor: (Integer, Integer) -> Integer |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
The following domains are used:
Integer
The ITRS R consists of the following rules:
92_0_descend_Load(
i12) →
181_0_descend_Return92_0_descend_Load(
i45) →
243_0_descend_Return92_0_descend_Load(
i59) →
256_0_descend_Return92_0_descend_Load(
i62) →
273_0_descend_Return92_0_descend_Load(
i67) →
287_0_descend_Return92_0_descend_Load(
i70) →
300_0_descend_Return92_0_descend_Load(
i74) →
314_0_descend_Return92_0_descend_Load(
i76) →
327_0_descend_Return92_0_descend_Load(
x0) →
169_0_descend_LE(
x0)
169_0_descend_LE(
0) →
175_0_descend_Return169_0_descend_LE(
x0) →
Cond_169_0_descend_LE(
x0 > 0,
x0)
Cond_169_0_descend_LE(
TRUE,
x0) →
191_1_descend_InvokeMethod(
169_0_descend_LE(
x0 - 1),
x0 - 1)
191_1_descend_InvokeMethod(
175_0_descend_Return,
0) →
220_0_descend_Return191_1_descend_InvokeMethod(
220_0_descend_Return,
x0) →
220_0_descend_ReturnThe integer pair graph contains the following rules and edges:
(10):
COND_321_2_REC_INVOKEMETHOD(
TRUE,
321_1_test_InvokeMethod(
220_0_descend_Return,
x0[10]),
x1[10],
x0[10]) →
69_0_REC_GE(
x1[10],
x0[10] + 1)
(9):
321_2_REC_INVOKEMETHOD(
321_1_test_InvokeMethod(
220_0_descend_Return,
x0[9]),
x1[9],
x0[9]) →
COND_321_2_REC_INVOKEMETHOD(
x0[9] > 0,
321_1_test_InvokeMethod(
220_0_descend_Return,
x0[9]),
x1[9],
x0[9])
(8):
309_2_REC_INVOKEMETHOD(
309_1_test_InvokeMethod(
220_0_descend_Return,
x0[8]),
x1[8],
x0[8]) →
321_2_REC_INVOKEMETHOD(
321_1_test_InvokeMethod(
92_0_descend_Load(
x0[8]),
x0[8]),
x1[8],
x0[8])
(7):
295_2_REC_INVOKEMETHOD(
295_1_test_InvokeMethod(
220_0_descend_Return,
x0[7]),
x1[7],
x0[7]) →
309_2_REC_INVOKEMETHOD(
309_1_test_InvokeMethod(
92_0_descend_Load(
x0[7]),
x0[7]),
x1[7],
x0[7])
(6):
282_2_REC_INVOKEMETHOD(
282_1_test_InvokeMethod(
220_0_descend_Return,
x0[6]),
x1[6],
x0[6]) →
295_2_REC_INVOKEMETHOD(
295_1_test_InvokeMethod(
92_0_descend_Load(
x0[6]),
x0[6]),
x1[6],
x0[6])
(5):
266_2_REC_INVOKEMETHOD(
266_1_test_InvokeMethod(
220_0_descend_Return,
x0[5]),
x1[5],
x0[5]) →
282_2_REC_INVOKEMETHOD(
282_1_test_InvokeMethod(
92_0_descend_Load(
x0[5]),
x0[5]),
x1[5],
x0[5])
(4):
250_2_REC_INVOKEMETHOD(
250_1_test_InvokeMethod(
220_0_descend_Return,
x0[4]),
x1[4],
x0[4]) →
266_2_REC_INVOKEMETHOD(
266_1_test_InvokeMethod(
92_0_descend_Load(
x0[4]),
x0[4]),
x1[4],
x0[4])
(3):
237_2_REC_INVOKEMETHOD(
237_1_test_InvokeMethod(
220_0_descend_Return,
x0[3]),
x1[3],
x0[3]) →
250_2_REC_INVOKEMETHOD(
250_1_test_InvokeMethod(
92_0_descend_Load(
x0[3]),
x0[3]),
x1[3],
x0[3])
(2):
92_2_REC_INVOKEMETHOD(
92_1_test_InvokeMethod(
220_0_descend_Return,
x0[2]),
x1[2],
x0[2]) →
237_2_REC_INVOKEMETHOD(
237_1_test_InvokeMethod(
92_0_descend_Load(
x0[2]),
x0[2]),
x1[2],
x0[2])
(1):
COND_69_0_REC_GE(
TRUE,
x0[1],
x1[1]) →
92_2_REC_INVOKEMETHOD(
92_1_test_InvokeMethod(
92_0_descend_Load(
x1[1]),
x1[1]),
x0[1],
x1[1])
(0):
69_0_REC_GE(
x0[0],
x1[0]) →
COND_69_0_REC_GE(
x1[0] < 100,
x0[0],
x1[0])
(10) -> (0), if ((x1[10] →* x0[0])∧(x0[10] + 1 →* x1[0]))
(0) -> (1), if ((x1[0] < 100 →* TRUE)∧(x0[0] →* x0[1])∧(x1[0] →* x1[1]))
(1) -> (2), if ((92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]) →* 92_1_test_InvokeMethod(220_0_descend_Return, x0[2]))∧(x0[1] →* x1[2])∧(x1[1] →* x0[2]))
(2) -> (3), if ((237_1_test_InvokeMethod(92_0_descend_Load(x0[2]), x0[2]) →* 237_1_test_InvokeMethod(220_0_descend_Return, x0[3]))∧(x1[2] →* x1[3])∧(x0[2] →* x0[3]))
(3) -> (4), if ((250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]) →* 250_1_test_InvokeMethod(220_0_descend_Return, x0[4]))∧(x1[3] →* x1[4])∧(x0[3] →* x0[4]))
(4) -> (5), if ((266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]) →* 266_1_test_InvokeMethod(220_0_descend_Return, x0[5]))∧(x1[4] →* x1[5])∧(x0[4] →* x0[5]))
(5) -> (6), if ((282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]) →* 282_1_test_InvokeMethod(220_0_descend_Return, x0[6]))∧(x1[5] →* x1[6])∧(x0[5] →* x0[6]))
(6) -> (7), if ((295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]) →* 295_1_test_InvokeMethod(220_0_descend_Return, x0[7]))∧(x1[6] →* x1[7])∧(x0[6] →* x0[7]))
(7) -> (8), if ((309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]) →* 309_1_test_InvokeMethod(220_0_descend_Return, x0[8]))∧(x1[7] →* x1[8])∧(x0[7] →* x0[8]))
(8) -> (9), if ((321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]) →* 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]))∧(x1[8] →* x1[9])∧(x0[8] →* x0[9]))
(9) -> (10), if ((x0[9] > 0 →* TRUE)∧(321_1_test_InvokeMethod(220_0_descend_Return, x0[9]) →* 321_1_test_InvokeMethod(220_0_descend_Return, x0[10]))∧(x1[9] →* x1[10])∧(x0[9] →* x0[10]))
The set Q consists of the following terms:
92_0_descend_Load(
x0)
97_1_rec_InvokeMethod(
47_0_rec_Return,
0)
97_1_rec_InvokeMethod(
143_0_rec_Return,
x0)
169_0_descend_LE(
x0)
Cond_169_0_descend_LE(
TRUE,
x0)
191_1_descend_InvokeMethod(
175_0_descend_Return,
0)
191_1_descend_InvokeMethod(
220_0_descend_Return,
x0)
(31) IDPNonInfProof (SOUND transformation)
The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that
final constraints are written in
bold face.
For Pair
COND_321_2_REC_INVOKEMETHOD(
TRUE,
321_1_test_InvokeMethod(
220_0_descend_Return,
x0[10]),
x1[10],
x0[10]) →
69_0_REC_GE(
x1[10],
+(
x0[10],
1)) the following chains were created:
- We consider the chain COND_321_2_REC_INVOKEMETHOD(TRUE, 321_1_test_InvokeMethod(220_0_descend_Return, x0[10]), x1[10], x0[10]) → 69_0_REC_GE(x1[10], +(x0[10], 1)) which results in the following constraint:
(1) (COND_321_2_REC_INVOKEMETHOD(TRUE, 321_1_test_InvokeMethod(220_0_descend_Return, x0[10]), x1[10], x0[10])≥NonInfC∧COND_321_2_REC_INVOKEMETHOD(TRUE, 321_1_test_InvokeMethod(220_0_descend_Return, x0[10]), x1[10], x0[10])≥69_0_REC_GE(x1[10], +(x0[10], 1))∧(UIncreasing(69_0_REC_GE(x1[10], +(x0[10], 1))), ≥))
We simplified constraint (1) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(2) ((UIncreasing(69_0_REC_GE(x1[10], +(x0[10], 1))), ≥)∧[(-1)bso_39] ≥ 0)
We simplified constraint (2) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(3) ((UIncreasing(69_0_REC_GE(x1[10], +(x0[10], 1))), ≥)∧[(-1)bso_39] ≥ 0)
We simplified constraint (3) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(4) ((UIncreasing(69_0_REC_GE(x1[10], +(x0[10], 1))), ≥)∧[(-1)bso_39] ≥ 0)
We simplified constraint (4) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(5) ((UIncreasing(69_0_REC_GE(x1[10], +(x0[10], 1))), ≥)∧0 = 0∧[(-1)bso_39] ≥ 0)
For Pair
321_2_REC_INVOKEMETHOD(
321_1_test_InvokeMethod(
220_0_descend_Return,
x0[9]),
x1[9],
x0[9]) →
COND_321_2_REC_INVOKEMETHOD(
>(
x0[9],
0),
321_1_test_InvokeMethod(
220_0_descend_Return,
x0[9]),
x1[9],
x0[9]) the following chains were created:
- We consider the chain 321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9]) → COND_321_2_REC_INVOKEMETHOD(>(x0[9], 0), 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9]), COND_321_2_REC_INVOKEMETHOD(TRUE, 321_1_test_InvokeMethod(220_0_descend_Return, x0[10]), x1[10], x0[10]) → 69_0_REC_GE(x1[10], +(x0[10], 1)) which results in the following constraint:
(6) (>(x0[9], 0)=TRUE∧321_1_test_InvokeMethod(220_0_descend_Return, x0[9])=321_1_test_InvokeMethod(220_0_descend_Return, x0[10])∧x1[9]=x1[10]∧x0[9]=x0[10] ⇒ 321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])≥NonInfC∧321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])≥COND_321_2_REC_INVOKEMETHOD(>(x0[9], 0), 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])∧(UIncreasing(COND_321_2_REC_INVOKEMETHOD(>(x0[9], 0), 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])), ≥))
We simplified constraint (6) using rules (I), (II), (IV), (DELETE_TRIVIAL_REDUCESTO) which results in the following new constraint:
(7) (>(x0[9], 0)=TRUE ⇒ 321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])≥NonInfC∧321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])≥COND_321_2_REC_INVOKEMETHOD(>(x0[9], 0), 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])∧(UIncreasing(COND_321_2_REC_INVOKEMETHOD(>(x0[9], 0), 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])), ≥))
We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(8) (x0[9] + [-1] ≥ 0 ⇒ (UIncreasing(COND_321_2_REC_INVOKEMETHOD(>(x0[9], 0), 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])), ≥)∧[(-1)bni_40 + (-1)Bound*bni_40] + [(-1)bni_40]x0[9] ≥ 0∧[(-1)bso_41] ≥ 0)
We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(9) (x0[9] + [-1] ≥ 0 ⇒ (UIncreasing(COND_321_2_REC_INVOKEMETHOD(>(x0[9], 0), 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])), ≥)∧[(-1)bni_40 + (-1)Bound*bni_40] + [(-1)bni_40]x0[9] ≥ 0∧[(-1)bso_41] ≥ 0)
We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(10) (x0[9] + [-1] ≥ 0 ⇒ (UIncreasing(COND_321_2_REC_INVOKEMETHOD(>(x0[9], 0), 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])), ≥)∧[(-1)bni_40 + (-1)Bound*bni_40] + [(-1)bni_40]x0[9] ≥ 0∧[(-1)bso_41] ≥ 0)
We simplified constraint (10) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(11) (x0[9] ≥ 0 ⇒ (UIncreasing(COND_321_2_REC_INVOKEMETHOD(>(x0[9], 0), 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])), ≥)∧[(-2)bni_40 + (-1)Bound*bni_40] + [(-1)bni_40]x0[9] ≥ 0∧[(-1)bso_41] ≥ 0)
For Pair
309_2_REC_INVOKEMETHOD(
309_1_test_InvokeMethod(
220_0_descend_Return,
x0[8]),
x1[8],
x0[8]) →
321_2_REC_INVOKEMETHOD(
321_1_test_InvokeMethod(
92_0_descend_Load(
x0[8]),
x0[8]),
x1[8],
x0[8]) the following chains were created:
- We consider the chain 309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(220_0_descend_Return, x0[8]), x1[8], x0[8]) → 321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]), x1[8], x0[8]) which results in the following constraint:
(12) (309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(220_0_descend_Return, x0[8]), x1[8], x0[8])≥NonInfC∧309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(220_0_descend_Return, x0[8]), x1[8], x0[8])≥321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]), x1[8], x0[8])∧(UIncreasing(321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]), x1[8], x0[8])), ≥))
We simplified constraint (12) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(13) ((UIncreasing(321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]), x1[8], x0[8])), ≥)∧[(-1)bso_43] ≥ 0)
We simplified constraint (13) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(14) ((UIncreasing(321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]), x1[8], x0[8])), ≥)∧[(-1)bso_43] ≥ 0)
We simplified constraint (14) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(15) ((UIncreasing(321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]), x1[8], x0[8])), ≥)∧[(-1)bso_43] ≥ 0)
We simplified constraint (15) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(16) ((UIncreasing(321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]), x1[8], x0[8])), ≥)∧0 = 0∧[(-1)bso_43] ≥ 0)
For Pair
295_2_REC_INVOKEMETHOD(
295_1_test_InvokeMethod(
220_0_descend_Return,
x0[7]),
x1[7],
x0[7]) →
309_2_REC_INVOKEMETHOD(
309_1_test_InvokeMethod(
92_0_descend_Load(
x0[7]),
x0[7]),
x1[7],
x0[7]) the following chains were created:
- We consider the chain 295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(220_0_descend_Return, x0[7]), x1[7], x0[7]) → 309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]), x1[7], x0[7]) which results in the following constraint:
(17) (295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(220_0_descend_Return, x0[7]), x1[7], x0[7])≥NonInfC∧295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(220_0_descend_Return, x0[7]), x1[7], x0[7])≥309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]), x1[7], x0[7])∧(UIncreasing(309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]), x1[7], x0[7])), ≥))
We simplified constraint (17) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(18) ((UIncreasing(309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]), x1[7], x0[7])), ≥)∧[(-1)bso_45] ≥ 0)
We simplified constraint (18) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(19) ((UIncreasing(309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]), x1[7], x0[7])), ≥)∧[(-1)bso_45] ≥ 0)
We simplified constraint (19) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(20) ((UIncreasing(309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]), x1[7], x0[7])), ≥)∧[(-1)bso_45] ≥ 0)
We simplified constraint (20) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(21) ((UIncreasing(309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]), x1[7], x0[7])), ≥)∧0 = 0∧[(-1)bso_45] ≥ 0)
For Pair
282_2_REC_INVOKEMETHOD(
282_1_test_InvokeMethod(
220_0_descend_Return,
x0[6]),
x1[6],
x0[6]) →
295_2_REC_INVOKEMETHOD(
295_1_test_InvokeMethod(
92_0_descend_Load(
x0[6]),
x0[6]),
x1[6],
x0[6]) the following chains were created:
- We consider the chain 282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(220_0_descend_Return, x0[6]), x1[6], x0[6]) → 295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]), x1[6], x0[6]) which results in the following constraint:
(22) (282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(220_0_descend_Return, x0[6]), x1[6], x0[6])≥NonInfC∧282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(220_0_descend_Return, x0[6]), x1[6], x0[6])≥295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]), x1[6], x0[6])∧(UIncreasing(295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]), x1[6], x0[6])), ≥))
We simplified constraint (22) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(23) ((UIncreasing(295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]), x1[6], x0[6])), ≥)∧[(-1)bso_47] ≥ 0)
We simplified constraint (23) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(24) ((UIncreasing(295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]), x1[6], x0[6])), ≥)∧[(-1)bso_47] ≥ 0)
We simplified constraint (24) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(25) ((UIncreasing(295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]), x1[6], x0[6])), ≥)∧[(-1)bso_47] ≥ 0)
We simplified constraint (25) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(26) ((UIncreasing(295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]), x1[6], x0[6])), ≥)∧0 = 0∧[(-1)bso_47] ≥ 0)
For Pair
266_2_REC_INVOKEMETHOD(
266_1_test_InvokeMethod(
220_0_descend_Return,
x0[5]),
x1[5],
x0[5]) →
282_2_REC_INVOKEMETHOD(
282_1_test_InvokeMethod(
92_0_descend_Load(
x0[5]),
x0[5]),
x1[5],
x0[5]) the following chains were created:
- We consider the chain 266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(220_0_descend_Return, x0[5]), x1[5], x0[5]) → 282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]), x1[5], x0[5]) which results in the following constraint:
(27) (266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(220_0_descend_Return, x0[5]), x1[5], x0[5])≥NonInfC∧266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(220_0_descend_Return, x0[5]), x1[5], x0[5])≥282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]), x1[5], x0[5])∧(UIncreasing(282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]), x1[5], x0[5])), ≥))
We simplified constraint (27) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(28) ((UIncreasing(282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]), x1[5], x0[5])), ≥)∧[(-1)bso_49] ≥ 0)
We simplified constraint (28) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(29) ((UIncreasing(282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]), x1[5], x0[5])), ≥)∧[(-1)bso_49] ≥ 0)
We simplified constraint (29) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(30) ((UIncreasing(282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]), x1[5], x0[5])), ≥)∧[(-1)bso_49] ≥ 0)
We simplified constraint (30) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(31) ((UIncreasing(282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]), x1[5], x0[5])), ≥)∧0 = 0∧[(-1)bso_49] ≥ 0)
For Pair
250_2_REC_INVOKEMETHOD(
250_1_test_InvokeMethod(
220_0_descend_Return,
x0[4]),
x1[4],
x0[4]) →
266_2_REC_INVOKEMETHOD(
266_1_test_InvokeMethod(
92_0_descend_Load(
x0[4]),
x0[4]),
x1[4],
x0[4]) the following chains were created:
- We consider the chain 250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(220_0_descend_Return, x0[4]), x1[4], x0[4]) → 266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]), x1[4], x0[4]) which results in the following constraint:
(32) (250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(220_0_descend_Return, x0[4]), x1[4], x0[4])≥NonInfC∧250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(220_0_descend_Return, x0[4]), x1[4], x0[4])≥266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]), x1[4], x0[4])∧(UIncreasing(266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]), x1[4], x0[4])), ≥))
We simplified constraint (32) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(33) ((UIncreasing(266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]), x1[4], x0[4])), ≥)∧[(-1)bso_51] ≥ 0)
We simplified constraint (33) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(34) ((UIncreasing(266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]), x1[4], x0[4])), ≥)∧[(-1)bso_51] ≥ 0)
We simplified constraint (34) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(35) ((UIncreasing(266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]), x1[4], x0[4])), ≥)∧[(-1)bso_51] ≥ 0)
We simplified constraint (35) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(36) ((UIncreasing(266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]), x1[4], x0[4])), ≥)∧0 = 0∧[(-1)bso_51] ≥ 0)
For Pair
237_2_REC_INVOKEMETHOD(
237_1_test_InvokeMethod(
220_0_descend_Return,
x0[3]),
x1[3],
x0[3]) →
250_2_REC_INVOKEMETHOD(
250_1_test_InvokeMethod(
92_0_descend_Load(
x0[3]),
x0[3]),
x1[3],
x0[3]) the following chains were created:
- We consider the chain 237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(220_0_descend_Return, x0[3]), x1[3], x0[3]) → 250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]), x1[3], x0[3]) which results in the following constraint:
(37) (237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(220_0_descend_Return, x0[3]), x1[3], x0[3])≥NonInfC∧237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(220_0_descend_Return, x0[3]), x1[3], x0[3])≥250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]), x1[3], x0[3])∧(UIncreasing(250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]), x1[3], x0[3])), ≥))
We simplified constraint (37) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(38) ((UIncreasing(250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]), x1[3], x0[3])), ≥)∧[(-1)bso_53] ≥ 0)
We simplified constraint (38) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(39) ((UIncreasing(250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]), x1[3], x0[3])), ≥)∧[(-1)bso_53] ≥ 0)
We simplified constraint (39) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(40) ((UIncreasing(250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]), x1[3], x0[3])), ≥)∧[(-1)bso_53] ≥ 0)
We simplified constraint (40) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(41) ((UIncreasing(250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]), x1[3], x0[3])), ≥)∧0 = 0∧[(-1)bso_53] ≥ 0)
For Pair
92_2_REC_INVOKEMETHOD(
92_1_test_InvokeMethod(
220_0_descend_Return,
x0[2]),
x1[2],
x0[2]) →
237_2_REC_INVOKEMETHOD(
237_1_test_InvokeMethod(
92_0_descend_Load(
x0[2]),
x0[2]),
x1[2],
x0[2]) the following chains were created:
- We consider the chain 92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(220_0_descend_Return, x0[2]), x1[2], x0[2]) → 237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(92_0_descend_Load(x0[2]), x0[2]), x1[2], x0[2]) which results in the following constraint:
(42) (92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(220_0_descend_Return, x0[2]), x1[2], x0[2])≥NonInfC∧92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(220_0_descend_Return, x0[2]), x1[2], x0[2])≥237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(92_0_descend_Load(x0[2]), x0[2]), x1[2], x0[2])∧(UIncreasing(237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(92_0_descend_Load(x0[2]), x0[2]), x1[2], x0[2])), ≥))
We simplified constraint (42) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(43) ((UIncreasing(237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(92_0_descend_Load(x0[2]), x0[2]), x1[2], x0[2])), ≥)∧[1 + (-1)bso_55] ≥ 0)
We simplified constraint (43) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(44) ((UIncreasing(237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(92_0_descend_Load(x0[2]), x0[2]), x1[2], x0[2])), ≥)∧[1 + (-1)bso_55] ≥ 0)
We simplified constraint (44) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(45) ((UIncreasing(237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(92_0_descend_Load(x0[2]), x0[2]), x1[2], x0[2])), ≥)∧[1 + (-1)bso_55] ≥ 0)
We simplified constraint (45) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(46) ((UIncreasing(237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(92_0_descend_Load(x0[2]), x0[2]), x1[2], x0[2])), ≥)∧0 = 0∧[1 + (-1)bso_55] ≥ 0)
For Pair
COND_69_0_REC_GE(
TRUE,
x0[1],
x1[1]) →
92_2_REC_INVOKEMETHOD(
92_1_test_InvokeMethod(
92_0_descend_Load(
x1[1]),
x1[1]),
x0[1],
x1[1]) the following chains were created:
- We consider the chain COND_69_0_REC_GE(TRUE, x0[1], x1[1]) → 92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]), x0[1], x1[1]) which results in the following constraint:
(47) (COND_69_0_REC_GE(TRUE, x0[1], x1[1])≥NonInfC∧COND_69_0_REC_GE(TRUE, x0[1], x1[1])≥92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]), x0[1], x1[1])∧(UIncreasing(92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]), x0[1], x1[1])), ≥))
We simplified constraint (47) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(48) ((UIncreasing(92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]), x0[1], x1[1])), ≥)∧[(-1)bso_57] ≥ 0)
We simplified constraint (48) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(49) ((UIncreasing(92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]), x0[1], x1[1])), ≥)∧[(-1)bso_57] ≥ 0)
We simplified constraint (49) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(50) ((UIncreasing(92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]), x0[1], x1[1])), ≥)∧[(-1)bso_57] ≥ 0)
We simplified constraint (50) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(51) ((UIncreasing(92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]), x0[1], x1[1])), ≥)∧0 = 0∧[(-1)bso_57] ≥ 0)
For Pair
69_0_REC_GE(
x0[0],
x1[0]) →
COND_69_0_REC_GE(
<(
x1[0],
100),
x0[0],
x1[0]) the following chains were created:
- We consider the chain 69_0_REC_GE(x0[0], x1[0]) → COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0]), COND_69_0_REC_GE(TRUE, x0[1], x1[1]) → 92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]), x0[1], x1[1]) which results in the following constraint:
(52) (<(x1[0], 100)=TRUE∧x0[0]=x0[1]∧x1[0]=x1[1] ⇒ 69_0_REC_GE(x0[0], x1[0])≥NonInfC∧69_0_REC_GE(x0[0], x1[0])≥COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])∧(UIncreasing(COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥))
We simplified constraint (52) using rule (IV) which results in the following new constraint:
(53) (<(x1[0], 100)=TRUE ⇒ 69_0_REC_GE(x0[0], x1[0])≥NonInfC∧69_0_REC_GE(x0[0], x1[0])≥COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])∧(UIncreasing(COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥))
We simplified constraint (53) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(54) ([99] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)Bound*bni_58] + [(-1)bni_58]x1[0] ≥ 0∧[(-1)bso_59] ≥ 0)
We simplified constraint (54) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(55) ([99] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)Bound*bni_58] + [(-1)bni_58]x1[0] ≥ 0∧[(-1)bso_59] ≥ 0)
We simplified constraint (55) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(56) ([99] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)Bound*bni_58] + [(-1)bni_58]x1[0] ≥ 0∧[(-1)bso_59] ≥ 0)
We simplified constraint (56) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
(57) ([99] + x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)Bound*bni_58] + [bni_58]x1[0] ≥ 0∧[(-1)bso_59] ≥ 0)
(58) ([99] + [-1]x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)Bound*bni_58] + [(-1)bni_58]x1[0] ≥ 0∧[(-1)bso_59] ≥ 0)
To summarize, we get the following constraints P
≥ for the following pairs.
- COND_321_2_REC_INVOKEMETHOD(TRUE, 321_1_test_InvokeMethod(220_0_descend_Return, x0[10]), x1[10], x0[10]) → 69_0_REC_GE(x1[10], +(x0[10], 1))
- ((UIncreasing(69_0_REC_GE(x1[10], +(x0[10], 1))), ≥)∧0 = 0∧[(-1)bso_39] ≥ 0)
- 321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9]) → COND_321_2_REC_INVOKEMETHOD(>(x0[9], 0), 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])
- (x0[9] ≥ 0 ⇒ (UIncreasing(COND_321_2_REC_INVOKEMETHOD(>(x0[9], 0), 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])), ≥)∧[(-2)bni_40 + (-1)Bound*bni_40] + [(-1)bni_40]x0[9] ≥ 0∧[(-1)bso_41] ≥ 0)
- 309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(220_0_descend_Return, x0[8]), x1[8], x0[8]) → 321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]), x1[8], x0[8])
- ((UIncreasing(321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]), x1[8], x0[8])), ≥)∧0 = 0∧[(-1)bso_43] ≥ 0)
- 295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(220_0_descend_Return, x0[7]), x1[7], x0[7]) → 309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]), x1[7], x0[7])
- ((UIncreasing(309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]), x1[7], x0[7])), ≥)∧0 = 0∧[(-1)bso_45] ≥ 0)
- 282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(220_0_descend_Return, x0[6]), x1[6], x0[6]) → 295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]), x1[6], x0[6])
- ((UIncreasing(295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]), x1[6], x0[6])), ≥)∧0 = 0∧[(-1)bso_47] ≥ 0)
- 266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(220_0_descend_Return, x0[5]), x1[5], x0[5]) → 282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]), x1[5], x0[5])
- ((UIncreasing(282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]), x1[5], x0[5])), ≥)∧0 = 0∧[(-1)bso_49] ≥ 0)
- 250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(220_0_descend_Return, x0[4]), x1[4], x0[4]) → 266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]), x1[4], x0[4])
- ((UIncreasing(266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]), x1[4], x0[4])), ≥)∧0 = 0∧[(-1)bso_51] ≥ 0)
- 237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(220_0_descend_Return, x0[3]), x1[3], x0[3]) → 250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]), x1[3], x0[3])
- ((UIncreasing(250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]), x1[3], x0[3])), ≥)∧0 = 0∧[(-1)bso_53] ≥ 0)
- 92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(220_0_descend_Return, x0[2]), x1[2], x0[2]) → 237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(92_0_descend_Load(x0[2]), x0[2]), x1[2], x0[2])
- ((UIncreasing(237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(92_0_descend_Load(x0[2]), x0[2]), x1[2], x0[2])), ≥)∧0 = 0∧[1 + (-1)bso_55] ≥ 0)
- COND_69_0_REC_GE(TRUE, x0[1], x1[1]) → 92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]), x0[1], x1[1])
- ((UIncreasing(92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]), x0[1], x1[1])), ≥)∧0 = 0∧[(-1)bso_57] ≥ 0)
- 69_0_REC_GE(x0[0], x1[0]) → COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])
- ([99] + x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)Bound*bni_58] + [bni_58]x1[0] ≥ 0∧[(-1)bso_59] ≥ 0)
- ([99] + [-1]x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)Bound*bni_58] + [(-1)bni_58]x1[0] ≥ 0∧[(-1)bso_59] ≥ 0)
The constraints for P
> respective P
bound are constructed from P
≥ where we just replace every occurence of "t ≥ s" in P
≥ by "t > s" respective "t ≥
c". Here
c stands for the fresh constant used for P
bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:
POL(TRUE) = 0
POL(FALSE) = 0
POL(92_0_descend_Load(x1)) = [-1] + x1
POL(181_0_descend_Return) = [1]
POL(243_0_descend_Return) = [1]
POL(256_0_descend_Return) = [1]
POL(273_0_descend_Return) = [1]
POL(287_0_descend_Return) = [2]
POL(300_0_descend_Return) = [-1]
POL(314_0_descend_Return) = [2]
POL(327_0_descend_Return) = [-1]
POL(169_0_descend_LE(x1)) = [-1] + [-1]x1
POL(0) = 0
POL(175_0_descend_Return) = [-1]
POL(Cond_169_0_descend_LE(x1, x2)) = [-1]
POL(>(x1, x2)) = [-1]
POL(191_1_descend_InvokeMethod(x1, x2)) = [2] + [-1]x2 + [-1]x1
POL(-(x1, x2)) = x1 + [-1]x2
POL(1) = [1]
POL(220_0_descend_Return) = [-1]
POL(COND_321_2_REC_INVOKEMETHOD(x1, x2, x3, x4)) = [-1] + [-1]x4
POL(321_1_test_InvokeMethod(x1, x2)) = [-1] + [2]x2 + [-1]x1
POL(69_0_REC_GE(x1, x2)) = [-1]x2
POL(+(x1, x2)) = x1 + x2
POL(321_2_REC_INVOKEMETHOD(x1, x2, x3)) = [-1] + [-1]x3
POL(309_2_REC_INVOKEMETHOD(x1, x2, x3)) = [-1] + [-1]x3
POL(309_1_test_InvokeMethod(x1, x2)) = [-1] + [-1]x2 + [-1]x1
POL(295_2_REC_INVOKEMETHOD(x1, x2, x3)) = [-1] + [-1]x3
POL(295_1_test_InvokeMethod(x1, x2)) = [-1] + [-1]x2 + [-1]x1
POL(282_2_REC_INVOKEMETHOD(x1, x2, x3)) = [-1] + [-1]x3
POL(282_1_test_InvokeMethod(x1, x2)) = [-1] + [2]x2 + [-1]x1
POL(266_2_REC_INVOKEMETHOD(x1, x2, x3)) = [-1] + [-1]x3
POL(266_1_test_InvokeMethod(x1, x2)) = [-1] + [-1]x2 + [-1]x1
POL(250_2_REC_INVOKEMETHOD(x1, x2, x3)) = [-1] + [-1]x3
POL(250_1_test_InvokeMethod(x1, x2)) = [-1] + [2]x2 + [-1]x1
POL(237_2_REC_INVOKEMETHOD(x1, x2, x3)) = [-1] + [-1]x3
POL(237_1_test_InvokeMethod(x1, x2)) = [-1] + [-1]x2 + [-1]x1
POL(92_2_REC_INVOKEMETHOD(x1, x2, x3)) = [-1]x1 + [-1]x3
POL(92_1_test_InvokeMethod(x1, x2)) = 0
POL(COND_69_0_REC_GE(x1, x2, x3)) = [-1]x3
POL(<(x1, x2)) = 0
POL(100) = [100]
The following pairs are in P
>:
92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(220_0_descend_Return, x0[2]), x1[2], x0[2]) → 237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(92_0_descend_Load(x0[2]), x0[2]), x1[2], x0[2])
The following pairs are in P
bound:
69_0_REC_GE(x0[0], x1[0]) → COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])
The following pairs are in P
≥:
COND_321_2_REC_INVOKEMETHOD(TRUE, 321_1_test_InvokeMethod(220_0_descend_Return, x0[10]), x1[10], x0[10]) → 69_0_REC_GE(x1[10], +(x0[10], 1))
321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9]) → COND_321_2_REC_INVOKEMETHOD(>(x0[9], 0), 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]), x1[9], x0[9])
309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(220_0_descend_Return, x0[8]), x1[8], x0[8]) → 321_2_REC_INVOKEMETHOD(321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]), x1[8], x0[8])
295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(220_0_descend_Return, x0[7]), x1[7], x0[7]) → 309_2_REC_INVOKEMETHOD(309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]), x1[7], x0[7])
282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(220_0_descend_Return, x0[6]), x1[6], x0[6]) → 295_2_REC_INVOKEMETHOD(295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]), x1[6], x0[6])
266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(220_0_descend_Return, x0[5]), x1[5], x0[5]) → 282_2_REC_INVOKEMETHOD(282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]), x1[5], x0[5])
250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(220_0_descend_Return, x0[4]), x1[4], x0[4]) → 266_2_REC_INVOKEMETHOD(266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]), x1[4], x0[4])
237_2_REC_INVOKEMETHOD(237_1_test_InvokeMethod(220_0_descend_Return, x0[3]), x1[3], x0[3]) → 250_2_REC_INVOKEMETHOD(250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]), x1[3], x0[3])
COND_69_0_REC_GE(TRUE, x0[1], x1[1]) → 92_2_REC_INVOKEMETHOD(92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]), x0[1], x1[1])
69_0_REC_GE(x0[0], x1[0]) → COND_69_0_REC_GE(<(x1[0], 100), x0[0], x1[0])
There are no usable rules.
(32) Complex Obligation (AND)
(33) Obligation:
IDP problem:
The following function symbols are pre-defined:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
| ~ | Bwxor: (Integer, Integer) -> Integer |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
The following domains are used:
Integer
The ITRS R consists of the following rules:
92_0_descend_Load(
i12) →
181_0_descend_Return92_0_descend_Load(
i45) →
243_0_descend_Return92_0_descend_Load(
i59) →
256_0_descend_Return92_0_descend_Load(
i62) →
273_0_descend_Return92_0_descend_Load(
i67) →
287_0_descend_Return92_0_descend_Load(
i70) →
300_0_descend_Return92_0_descend_Load(
i74) →
314_0_descend_Return92_0_descend_Load(
i76) →
327_0_descend_Return92_0_descend_Load(
x0) →
169_0_descend_LE(
x0)
169_0_descend_LE(
0) →
175_0_descend_Return169_0_descend_LE(
x0) →
Cond_169_0_descend_LE(
x0 > 0,
x0)
Cond_169_0_descend_LE(
TRUE,
x0) →
191_1_descend_InvokeMethod(
169_0_descend_LE(
x0 - 1),
x0 - 1)
191_1_descend_InvokeMethod(
175_0_descend_Return,
0) →
220_0_descend_Return191_1_descend_InvokeMethod(
220_0_descend_Return,
x0) →
220_0_descend_ReturnThe integer pair graph contains the following rules and edges:
(10):
COND_321_2_REC_INVOKEMETHOD(
TRUE,
321_1_test_InvokeMethod(
220_0_descend_Return,
x0[10]),
x1[10],
x0[10]) →
69_0_REC_GE(
x1[10],
x0[10] + 1)
(9):
321_2_REC_INVOKEMETHOD(
321_1_test_InvokeMethod(
220_0_descend_Return,
x0[9]),
x1[9],
x0[9]) →
COND_321_2_REC_INVOKEMETHOD(
x0[9] > 0,
321_1_test_InvokeMethod(
220_0_descend_Return,
x0[9]),
x1[9],
x0[9])
(8):
309_2_REC_INVOKEMETHOD(
309_1_test_InvokeMethod(
220_0_descend_Return,
x0[8]),
x1[8],
x0[8]) →
321_2_REC_INVOKEMETHOD(
321_1_test_InvokeMethod(
92_0_descend_Load(
x0[8]),
x0[8]),
x1[8],
x0[8])
(7):
295_2_REC_INVOKEMETHOD(
295_1_test_InvokeMethod(
220_0_descend_Return,
x0[7]),
x1[7],
x0[7]) →
309_2_REC_INVOKEMETHOD(
309_1_test_InvokeMethod(
92_0_descend_Load(
x0[7]),
x0[7]),
x1[7],
x0[7])
(6):
282_2_REC_INVOKEMETHOD(
282_1_test_InvokeMethod(
220_0_descend_Return,
x0[6]),
x1[6],
x0[6]) →
295_2_REC_INVOKEMETHOD(
295_1_test_InvokeMethod(
92_0_descend_Load(
x0[6]),
x0[6]),
x1[6],
x0[6])
(5):
266_2_REC_INVOKEMETHOD(
266_1_test_InvokeMethod(
220_0_descend_Return,
x0[5]),
x1[5],
x0[5]) →
282_2_REC_INVOKEMETHOD(
282_1_test_InvokeMethod(
92_0_descend_Load(
x0[5]),
x0[5]),
x1[5],
x0[5])
(4):
250_2_REC_INVOKEMETHOD(
250_1_test_InvokeMethod(
220_0_descend_Return,
x0[4]),
x1[4],
x0[4]) →
266_2_REC_INVOKEMETHOD(
266_1_test_InvokeMethod(
92_0_descend_Load(
x0[4]),
x0[4]),
x1[4],
x0[4])
(3):
237_2_REC_INVOKEMETHOD(
237_1_test_InvokeMethod(
220_0_descend_Return,
x0[3]),
x1[3],
x0[3]) →
250_2_REC_INVOKEMETHOD(
250_1_test_InvokeMethod(
92_0_descend_Load(
x0[3]),
x0[3]),
x1[3],
x0[3])
(1):
COND_69_0_REC_GE(
TRUE,
x0[1],
x1[1]) →
92_2_REC_INVOKEMETHOD(
92_1_test_InvokeMethod(
92_0_descend_Load(
x1[1]),
x1[1]),
x0[1],
x1[1])
(0):
69_0_REC_GE(
x0[0],
x1[0]) →
COND_69_0_REC_GE(
x1[0] < 100,
x0[0],
x1[0])
(10) -> (0), if ((x1[10] →* x0[0])∧(x0[10] + 1 →* x1[0]))
(0) -> (1), if ((x1[0] < 100 →* TRUE)∧(x0[0] →* x0[1])∧(x1[0] →* x1[1]))
(3) -> (4), if ((250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]) →* 250_1_test_InvokeMethod(220_0_descend_Return, x0[4]))∧(x1[3] →* x1[4])∧(x0[3] →* x0[4]))
(4) -> (5), if ((266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]) →* 266_1_test_InvokeMethod(220_0_descend_Return, x0[5]))∧(x1[4] →* x1[5])∧(x0[4] →* x0[5]))
(5) -> (6), if ((282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]) →* 282_1_test_InvokeMethod(220_0_descend_Return, x0[6]))∧(x1[5] →* x1[6])∧(x0[5] →* x0[6]))
(6) -> (7), if ((295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]) →* 295_1_test_InvokeMethod(220_0_descend_Return, x0[7]))∧(x1[6] →* x1[7])∧(x0[6] →* x0[7]))
(7) -> (8), if ((309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]) →* 309_1_test_InvokeMethod(220_0_descend_Return, x0[8]))∧(x1[7] →* x1[8])∧(x0[7] →* x0[8]))
(8) -> (9), if ((321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]) →* 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]))∧(x1[8] →* x1[9])∧(x0[8] →* x0[9]))
(9) -> (10), if ((x0[9] > 0 →* TRUE)∧(321_1_test_InvokeMethod(220_0_descend_Return, x0[9]) →* 321_1_test_InvokeMethod(220_0_descend_Return, x0[10]))∧(x1[9] →* x1[10])∧(x0[9] →* x0[10]))
The set Q consists of the following terms:
92_0_descend_Load(
x0)
97_1_rec_InvokeMethod(
47_0_rec_Return,
0)
97_1_rec_InvokeMethod(
143_0_rec_Return,
x0)
169_0_descend_LE(
x0)
Cond_169_0_descend_LE(
TRUE,
x0)
191_1_descend_InvokeMethod(
175_0_descend_Return,
0)
191_1_descend_InvokeMethod(
220_0_descend_Return,
x0)
(34) IDependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 10 less nodes.
(35) TRUE
(36) Obligation:
IDP problem:
The following function symbols are pre-defined:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
| ~ | Bwxor: (Integer, Integer) -> Integer |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
The following domains are used:
Integer
The ITRS R consists of the following rules:
92_0_descend_Load(
i12) →
181_0_descend_Return92_0_descend_Load(
i45) →
243_0_descend_Return92_0_descend_Load(
i59) →
256_0_descend_Return92_0_descend_Load(
i62) →
273_0_descend_Return92_0_descend_Load(
i67) →
287_0_descend_Return92_0_descend_Load(
i70) →
300_0_descend_Return92_0_descend_Load(
i74) →
314_0_descend_Return92_0_descend_Load(
i76) →
327_0_descend_Return92_0_descend_Load(
x0) →
169_0_descend_LE(
x0)
169_0_descend_LE(
0) →
175_0_descend_Return169_0_descend_LE(
x0) →
Cond_169_0_descend_LE(
x0 > 0,
x0)
Cond_169_0_descend_LE(
TRUE,
x0) →
191_1_descend_InvokeMethod(
169_0_descend_LE(
x0 - 1),
x0 - 1)
191_1_descend_InvokeMethod(
175_0_descend_Return,
0) →
220_0_descend_Return191_1_descend_InvokeMethod(
220_0_descend_Return,
x0) →
220_0_descend_ReturnThe integer pair graph contains the following rules and edges:
(10):
COND_321_2_REC_INVOKEMETHOD(
TRUE,
321_1_test_InvokeMethod(
220_0_descend_Return,
x0[10]),
x1[10],
x0[10]) →
69_0_REC_GE(
x1[10],
x0[10] + 1)
(9):
321_2_REC_INVOKEMETHOD(
321_1_test_InvokeMethod(
220_0_descend_Return,
x0[9]),
x1[9],
x0[9]) →
COND_321_2_REC_INVOKEMETHOD(
x0[9] > 0,
321_1_test_InvokeMethod(
220_0_descend_Return,
x0[9]),
x1[9],
x0[9])
(8):
309_2_REC_INVOKEMETHOD(
309_1_test_InvokeMethod(
220_0_descend_Return,
x0[8]),
x1[8],
x0[8]) →
321_2_REC_INVOKEMETHOD(
321_1_test_InvokeMethod(
92_0_descend_Load(
x0[8]),
x0[8]),
x1[8],
x0[8])
(7):
295_2_REC_INVOKEMETHOD(
295_1_test_InvokeMethod(
220_0_descend_Return,
x0[7]),
x1[7],
x0[7]) →
309_2_REC_INVOKEMETHOD(
309_1_test_InvokeMethod(
92_0_descend_Load(
x0[7]),
x0[7]),
x1[7],
x0[7])
(6):
282_2_REC_INVOKEMETHOD(
282_1_test_InvokeMethod(
220_0_descend_Return,
x0[6]),
x1[6],
x0[6]) →
295_2_REC_INVOKEMETHOD(
295_1_test_InvokeMethod(
92_0_descend_Load(
x0[6]),
x0[6]),
x1[6],
x0[6])
(5):
266_2_REC_INVOKEMETHOD(
266_1_test_InvokeMethod(
220_0_descend_Return,
x0[5]),
x1[5],
x0[5]) →
282_2_REC_INVOKEMETHOD(
282_1_test_InvokeMethod(
92_0_descend_Load(
x0[5]),
x0[5]),
x1[5],
x0[5])
(4):
250_2_REC_INVOKEMETHOD(
250_1_test_InvokeMethod(
220_0_descend_Return,
x0[4]),
x1[4],
x0[4]) →
266_2_REC_INVOKEMETHOD(
266_1_test_InvokeMethod(
92_0_descend_Load(
x0[4]),
x0[4]),
x1[4],
x0[4])
(3):
237_2_REC_INVOKEMETHOD(
237_1_test_InvokeMethod(
220_0_descend_Return,
x0[3]),
x1[3],
x0[3]) →
250_2_REC_INVOKEMETHOD(
250_1_test_InvokeMethod(
92_0_descend_Load(
x0[3]),
x0[3]),
x1[3],
x0[3])
(2):
92_2_REC_INVOKEMETHOD(
92_1_test_InvokeMethod(
220_0_descend_Return,
x0[2]),
x1[2],
x0[2]) →
237_2_REC_INVOKEMETHOD(
237_1_test_InvokeMethod(
92_0_descend_Load(
x0[2]),
x0[2]),
x1[2],
x0[2])
(1):
COND_69_0_REC_GE(
TRUE,
x0[1],
x1[1]) →
92_2_REC_INVOKEMETHOD(
92_1_test_InvokeMethod(
92_0_descend_Load(
x1[1]),
x1[1]),
x0[1],
x1[1])
(1) -> (2), if ((92_1_test_InvokeMethod(92_0_descend_Load(x1[1]), x1[1]) →* 92_1_test_InvokeMethod(220_0_descend_Return, x0[2]))∧(x0[1] →* x1[2])∧(x1[1] →* x0[2]))
(2) -> (3), if ((237_1_test_InvokeMethod(92_0_descend_Load(x0[2]), x0[2]) →* 237_1_test_InvokeMethod(220_0_descend_Return, x0[3]))∧(x1[2] →* x1[3])∧(x0[2] →* x0[3]))
(3) -> (4), if ((250_1_test_InvokeMethod(92_0_descend_Load(x0[3]), x0[3]) →* 250_1_test_InvokeMethod(220_0_descend_Return, x0[4]))∧(x1[3] →* x1[4])∧(x0[3] →* x0[4]))
(4) -> (5), if ((266_1_test_InvokeMethod(92_0_descend_Load(x0[4]), x0[4]) →* 266_1_test_InvokeMethod(220_0_descend_Return, x0[5]))∧(x1[4] →* x1[5])∧(x0[4] →* x0[5]))
(5) -> (6), if ((282_1_test_InvokeMethod(92_0_descend_Load(x0[5]), x0[5]) →* 282_1_test_InvokeMethod(220_0_descend_Return, x0[6]))∧(x1[5] →* x1[6])∧(x0[5] →* x0[6]))
(6) -> (7), if ((295_1_test_InvokeMethod(92_0_descend_Load(x0[6]), x0[6]) →* 295_1_test_InvokeMethod(220_0_descend_Return, x0[7]))∧(x1[6] →* x1[7])∧(x0[6] →* x0[7]))
(7) -> (8), if ((309_1_test_InvokeMethod(92_0_descend_Load(x0[7]), x0[7]) →* 309_1_test_InvokeMethod(220_0_descend_Return, x0[8]))∧(x1[7] →* x1[8])∧(x0[7] →* x0[8]))
(8) -> (9), if ((321_1_test_InvokeMethod(92_0_descend_Load(x0[8]), x0[8]) →* 321_1_test_InvokeMethod(220_0_descend_Return, x0[9]))∧(x1[8] →* x1[9])∧(x0[8] →* x0[9]))
(9) -> (10), if ((x0[9] > 0 →* TRUE)∧(321_1_test_InvokeMethod(220_0_descend_Return, x0[9]) →* 321_1_test_InvokeMethod(220_0_descend_Return, x0[10]))∧(x1[9] →* x1[10])∧(x0[9] →* x0[10]))
The set Q consists of the following terms:
92_0_descend_Load(
x0)
97_1_rec_InvokeMethod(
47_0_rec_Return,
0)
97_1_rec_InvokeMethod(
143_0_rec_Return,
x0)
169_0_descend_LE(
x0)
Cond_169_0_descend_LE(
TRUE,
x0)
191_1_descend_InvokeMethod(
175_0_descend_Return,
0)
191_1_descend_InvokeMethod(
220_0_descend_Return,
x0)
(37) IDependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 10 less nodes.
(38) TRUE